let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for p1, p2, q1, q2 being FinSequence of FreeAtoms H st p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H holds
p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H
let H be Group-like associative multMagma-Family of I; :: thesis: for p1, p2, q1, q2 being FinSequence of FreeAtoms H st p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H holds
p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H
let p1, p2, q1, q2 be FinSequence of FreeAtoms H; :: thesis: ( p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H implies p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H )
assume ( p1,q1 are_convertible_wrt ReductionRel H & p2,q2 are_convertible_wrt ReductionRel H ) ; :: thesis: p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H
then A1: ( p1,q1 are_convergent_wrt ReductionRel H & p2,q2 are_convergent_wrt ReductionRel H ) by REWRITE1:def 23;
then consider c1 being object such that
A2: ( ReductionRel H reduces p1,c1 & ReductionRel H reduces q1,c1 ) by REWRITE1:def 7;
p1 in (FreeAtoms H) * by FINSEQ_1:def 11;
then p1 in field (ReductionRel H) by Th30;
then c1 in field (ReductionRel H) by A2, REWRITE1:19;
then c1 in (FreeAtoms H) * by Th30;
then reconsider c1 = c1 as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
consider c2 being object such that
A3: ( ReductionRel H reduces p2,c2 & ReductionRel H reduces q2,c2 ) by A1, REWRITE1:def 7;
p2 in (FreeAtoms H) * by FINSEQ_1:def 11;
then p2 in field (ReductionRel H) by Th30;
then c2 in field (ReductionRel H) by A3, REWRITE1:19;
then c2 in (FreeAtoms H) * by Th30;
then reconsider c2 = c2 as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
ReductionRel H reduces p1 ^ p2,c1 ^ c2 by A2, A3, Th41;
then A4: p1 ^ p2,c1 ^ c2 are_convertible_wrt ReductionRel H by REWRITE1:25;
ReductionRel H reduces q1 ^ q2,c1 ^ c2 by A2, A3, Th41;
then c1 ^ c2,q1 ^ q2 are_convertible_wrt ReductionRel H by REWRITE1:25;
hence p1 ^ p2,q1 ^ q2 are_convertible_wrt ReductionRel H by A4, REWRITE1:30; :: thesis: verum