let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I
for p, q being FinSequence of FreeAtoms G holds [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms G holds [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G
let p, q be FinSequence of FreeAtoms G; :: thesis: [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G
[i,(1_ (G . i))] in FreeAtoms G by Th9;
then reconsider s = <*[i,(1_ (G . i))]*> as FinSequence of FreeAtoms G by FINSEQ_1:74;
(p ^ s) ^ q is FinSequence of FreeAtoms G ;
hence [((p ^ <*[i,(1_ (G . i))]*>) ^ q),(p ^ q)] in ReductionRel G by Def3; :: thesis: verum