let I be non empty set ; :: thesis: for i being Element of I
for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds <*[i,g]*> in [*i,g*]
let i be Element of I; :: thesis: for H being Group-like associative multMagma-Family of I
for g being Element of (H . i) holds <*[i,g]*> in [*i,g*]
let H be Group-like associative multMagma-Family of I; :: thesis: for g being Element of (H . i) holds <*[i,g]*> in [*i,g*]
let g be Element of (H . i); :: thesis: <*[i,g]*> in [*i,g*]
[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 <*[i,g]*> in [*i,g*] by EQREL_1:20; :: thesis: verum