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) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q
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) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q
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) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q
let p, q be FinSequence of FreeAtoms G; :: thesis: for g, h being Element of (G . i) st g * h = 1_ (G . i) holds
ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q
let g, h be Element of (G . i); :: thesis: ( g * h = 1_ (G . i) implies ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q )
assume A1: g * h = 1_ (G . i) ; :: thesis: ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q
[((p ^ <*[i,g],[i,h]*>) ^ q),((p ^ <*[i,(g * h)]*>) ^ q)] in ReductionRel G by Th26;
then A2: ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,(p ^ <*[i,(g * h)]*>) ^ q by REWRITE1:15;
[((p ^ <*[i,(g * h)]*>) ^ q),(p ^ q)] in ReductionRel G by A1, Th28;
then ReductionRel G reduces (p ^ <*[i,(g * h)]*>) ^ q,p ^ q by REWRITE1:15;
hence ReductionRel G reduces (p ^ <*[i,g],[i,h]*>) ^ q,p ^ q by A2, REWRITE1:16; :: thesis: verum