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