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
for g, h being Element of (G . i) holds [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ 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
for g, h being Element of (G . i) holds [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms G
for g, h being Element of (G . i) holds [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G
let p, q be FinSequence of FreeAtoms G; :: thesis: for g, h being Element of (G . i) holds [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G
let g, h be Element of (G . i); :: thesis: [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G
( [i,g] in FreeAtoms G & [i,h] in FreeAtoms G & [i,(g * h)] in FreeAtoms G ) by Th9;
then reconsider s = <*[i,g],[i,h]*>, t = <*[i,(g * h)]*> as FinSequence of FreeAtoms G by FINSEQ_1:74, FINSEQ_2:13;
( (p ^ s) ^ q is FinSequence of FreeAtoms G & (p ^ t) ^ q is FinSequence of FreeAtoms G ) ;
hence [((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G by Def3; :: thesis: verum