[i,g] in FreeAtoms H by Th9;
then <*[i,g]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
then <*[i,g]*> in (FreeAtoms H) * by FINSEQ_1:def 11;
then <*[i,g]*> in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
hence Class ((EqCl (ReductionRel H)),<*[i,g]*>) is Element of (FreeProduct H) by EQREL_1:def 3; :: thesis: verum