let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I holds [*i,(1_ (H . i))*] = 1_ (FreeProduct H)
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I holds [*i,(1_ (H . i))*] = 1_ (FreeProduct H)
let H be Group-like associative multMagma-Family of I; :: thesis: [*i,(1_ (H . i))*] = 1_ (FreeProduct H)
[i,(1_ (H . i))] in FreeAtoms H by Th9;
then <*[i,(1_ (H . i))]*> is FinSequence of FreeAtoms H by FINSEQ_1:74;
then <*[i,(1_ (H . i))]*> in (FreeAtoms H) * by FINSEQ_1:def 11;
then A1: <*[i,(1_ (H . i))]*> in the carrier of ((FreeAtoms H) *+^+<0>) by MONOID_0:61;
A2: [<*[i,(1_ (H . i))]*>,{}] in ReductionRel H by Th29;
ReductionRel H c= EqCl (ReductionRel H) by MSUALG_5:def 1;
then Class ((EqCl (ReductionRel H)),{}) = [*i,(1_ (H . i))*] by A1, A2, EQREL_1:35;
hence [*i,(1_ (H . i))*] = 1_ (FreeProduct H) by Th45; :: thesis: verum