let I be non empty set ; :: thesis: for i being Element of I
for G being Group-like multMagma-Family of I
for g, h being Element of (G . i) holds [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G
let i be Element of I; :: thesis: for G being Group-like multMagma-Family of I
for g, h being Element of (G . i) holds [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G
let G be Group-like multMagma-Family of I; :: thesis: for g, h being Element of (G . i) holds [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G
let g, h be Element of (G . i); :: thesis: [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G
set p = <*> (FreeAtoms G);
[(((<*> (FreeAtoms G)) ^ <*[i,g],[i,h]*>) ^ (<*> (FreeAtoms G))),(((<*> (FreeAtoms G)) ^ <*[i,(g * h)]*>) ^ (<*> (FreeAtoms G)))] = [(<*[i,g],[i,h]*> ^ (<*> (FreeAtoms G))),(((<*> (FreeAtoms G)) ^ <*[i,(g * h)]*>) ^ (<*> (FreeAtoms G)))] by FINSEQ_1:34
.= [<*[i,g],[i,h]*>,(((<*> (FreeAtoms G)) ^ <*[i,(g * h)]*>) ^ (<*> (FreeAtoms G)))] by FINSEQ_1:34
.= [<*[i,g],[i,h]*>,(<*[i,(g * h)]*> ^ (<*> (FreeAtoms G)))] by FINSEQ_1:34
.= [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] by FINSEQ_1:34 ;
hence [<*[i,g],[i,h]*>,<*[i,(g * h)]*>] in ReductionRel G by Th26; :: thesis: verum