set C = the carrier of (H . i);
rng (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) = 1 -tuples_on [:{i}, the carrier of (H . i):] by Th55;
then A1: rng (curry' (uncurry <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>)) c= (FreeAtoms H) * by Lm4;
dom (proj (Class (EqCl (ReductionRel H)))) = the carrier of ((FreeAtoms H) *+^+<0>) by FUNCT_2:def 1
.= (FreeAtoms H) * by MONOID_0:61 ;
then A2: dom ((proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>)) = dom (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) by A1, RELAT_1:27
.= the carrier of (H . i) by Th53 ;
rng ((proj (Class (EqCl (ReductionRel H)))) * (curry' (uncurry <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>))) c= the carrier of (FreeProduct H) ;
hence (proj (Class (EqCl (ReductionRel H)))) * (commute <*<:( the carrier of (H . i) --> i),(id the carrier of (H . i)):>*>) is Function of (H . i),(FreeProduct H) by A2, FUNCT_2:2; :: thesis: verum