let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I
for p, q, r being FinSequence of FreeAtoms G st [p,q] in ReductionRel G holds
( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )
let G be Group-like multMagma-Family of I; :: thesis: for p, q, r being FinSequence of FreeAtoms G st [p,q] in ReductionRel G holds
( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )
let p, q, r be FinSequence of FreeAtoms G; :: thesis: ( [p,q] in ReductionRel G implies ( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G ) )
assume [p,q] in ReductionRel G ; :: thesis: ( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )

per cases then ( ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) or ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ) by Def3;

suppose ex s, t being FinSequence of FreeAtoms G ex i being Element of I st
( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) ; :: thesis: ( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )

then consider s, t being FinSequence of FreeAtoms G, i being Element of I such that
A1: ( p = (s ^ <*[i,(1_ (G . i))]*>) ^ t & q = s ^ t ) ;
A2: p ^ r = (s ^ <*[i,(1_ (G . i))]*>) ^ (t ^ r) by A1, FINSEQ_1:32;
q ^ r = s ^ (t ^ r) by A1, FINSEQ_1:32;
hence [(p ^ r),(q ^ r)] in ReductionRel G by A2, Def3; :: thesis: [(r ^ p),(r ^ q)] in ReductionRel G
A3: r ^ p = (r ^ (s ^ <*[i,(1_ (G . i))]*>)) ^ t by A1, FINSEQ_1:32
.= ((r ^ s) ^ <*[i,(1_ (G . i))]*>) ^ t by FINSEQ_1:32 ;
r ^ q = (r ^ s) ^ t by A1, FINSEQ_1:32;
hence [(r ^ p),(r ^ q)] in ReductionRel G by A3, Def3; :: thesis: verum

end;

suppose ex s, t being FinSequence of FreeAtoms G ex i being Element of I ex g, h being Element of (G . i) st
( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ; :: thesis: ( [(p ^ r),(q ^ r)] in ReductionRel G & [(r ^ p),(r ^ q)] in ReductionRel G )

then consider s, t being FinSequence of FreeAtoms G, i being Element of I, g, h being Element of (G . i) such that
A4: ( p = (s ^ <*[i,g],[i,h]*>) ^ t & q = (s ^ <*[i,(g * h)]*>) ^ t ) ;
A5: p ^ r = (s ^ <*[i,g],[i,h]*>) ^ (t ^ r) by A4, FINSEQ_1:32;
q ^ r = (s ^ <*[i,(g * h)]*>) ^ (t ^ r) by A4, FINSEQ_1:32;
hence [(p ^ r),(q ^ r)] in ReductionRel G by A5, Def3; :: thesis: [(r ^ p),(r ^ q)] in ReductionRel G
A6: r ^ p = (r ^ (s ^ <*[i,g],[i,h]*>)) ^ t by A4, FINSEQ_1:32
.= ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t by FINSEQ_1:32 ;
r ^ q = (r ^ (s ^ <*[i,(g * h)]*>)) ^ t by A4, FINSEQ_1:32
.= ((r ^ s) ^ <*[i,(g * h)]*>) ^ t by FINSEQ_1:32 ;
hence [(r ^ p),(r ^ q)] in ReductionRel G by A6, Def3; :: thesis: verum

end;

end;