let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> is FinSequence of FreeAtoms G
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I
for g being Element of (G . i) holds <*[i,g]*> is FinSequence of FreeAtoms G
let G be Group-like multMagma-Family of I; :: thesis: for g being Element of (G . i) holds <*[i,g]*> is FinSequence of FreeAtoms G
let g be Element of (G . i); :: thesis: <*[i,g]*> is FinSequence of FreeAtoms G
[i,g] in FreeAtoms G by Th9;
hence <*[i,g]*> is FinSequence of FreeAtoms G by FINSEQ_1:74; :: thesis: verum