« Dirichlet Product of Species
Lemma.
Identity type of cartesian decomposition with FTIT
[00EL]
see folder.