let I be non empty set ; :: thesis: for G being Group-like multMagma-Family of I
for p1, p2, q1, q2 being FinSequence of FreeAtoms G st ReductionRel G reduces p1,q1 & ReductionRel G reduces p2,q2 holds
ReductionRel G reduces p1 ^ p2,q1 ^ q2
let G be Group-like multMagma-Family of I; :: thesis: for p1, p2, q1, q2 being FinSequence of FreeAtoms G st ReductionRel G reduces p1,q1 & ReductionRel G reduces p2,q2 holds
ReductionRel G reduces p1 ^ p2,q1 ^ q2
let p1, p2, q1, q2 be FinSequence of FreeAtoms G; :: thesis: ( ReductionRel G reduces p1,q1 & ReductionRel G reduces p2,q2 implies ReductionRel G reduces p1 ^ p2,q1 ^ q2 )
assume ReductionRel G reduces p1,q1 ; :: thesis: ( not ReductionRel G reduces p2,q2 or ReductionRel G reduces p1 ^ p2,q1 ^ q2 )
then consider R1 being RedSequence of ReductionRel G such that
A1: ( R1 . 1 = p1 & R1 . (len R1) = q1 ) by REWRITE1:def 3;
assume ReductionRel G reduces p2,q2 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2
then consider R2 being RedSequence of ReductionRel G such that
A2: ( R2 . 1 = p2 & R2 . (len R2) = q2 ) by REWRITE1:def 3;

per cases ( p1 = q1 or p1 <> q1 ) ;

suppose A3: p1 = q1 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

per cases ( p2 = q2 or p2 <> q2 ) ;

suppose p2 = q2 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

hence ReductionRel G reduces p1 ^ p2,q1 ^ q2 by A3, REWRITE1:12; :: thesis: verum

end;

suppose p2 <> q2 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

then not R2 is trivial by A2, NAT_1:23, NAT_D:60;
then reconsider R2 = R2 as FinSequence-yielding FinSequence ;
deffunc H₁( object ) -> set = q1 ^ (R2 . $1);
consider S2 being FinSequence such that
A4: ( len S2 = len R2 & ( for k being Nat st k in dom S2 holds
S2 . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A5: len S2 > 0 by A4;

now :: thesis: for k being Nat st k in dom S2 & k + 1 in dom S2 holds
[(S2 . k),(S2 . (k + 1))] in ReductionRel G

let k be Nat; :: thesis: ( k in dom S2 & k + 1 in dom S2 implies [(S2 . k),(S2 . (k + 1))] in ReductionRel G )
assume A6: ( k in dom S2 & k + 1 in dom S2 ) ; :: thesis: [(S2 . k),(S2 . (k + 1))] in ReductionRel G
dom S2 = dom R2 by A4, FINSEQ_3:29;
then A7: [(R2 . k),(R2 . (k + 1))] in ReductionRel G by A6, REWRITE1:def 2;
then ( R2 . k is FinSequence of FreeAtoms G & R2 . (k + 1) is FinSequence of FreeAtoms G ) by Th31;
then A8: [(q1 ^ (R2 . k)),(q1 ^ (R2 . (k + 1)))] in ReductionRel G by A7, Th25;
( q1 ^ (R2 . k) = S2 . k & q1 ^ (R2 . (k + 1)) = S2 . (k + 1) ) by A4, A6;
hence [(S2 . k),(S2 . (k + 1))] in ReductionRel G by A8; :: thesis: verum

end;

then reconsider S2 = S2 as RedSequence of ReductionRel G by A5, REWRITE1:def 2;
0 + 1 < (len S2) + 1 by XREAL_1:6;
then 1 <= len S2 by NAT_1:13;
then A9: ( 1 in dom S2 & len S2 in dom S2 ) by FINSEQ_3:25;
then A10: S2 . 1 = p1 ^ p2 by A2, A3, A4;
S2 . (len S2) = q1 ^ q2 by A2, A4, A9;
hence ReductionRel G reduces p1 ^ p2,q1 ^ q2 by A10, REWRITE1:def 3; :: thesis: verum

end;

end;

end;

suppose p1 <> q1 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

then A11: 1 <> len R1 by A1;
A12: 2 <= len R1 by A11, NAT_1:23;
then not R1 is trivial by NAT_D:60;
then reconsider R1 = R1 as FinSequence-yielding FinSequence ;
deffunc H₁( object ) -> set = (R1 . $1) ^ p2;
consider S1 being FinSequence such that
A13: ( len S1 = len R1 & ( for k being Nat st k in dom S1 holds
S1 . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A14: len S1 > 0 by A13;

now :: thesis: for k being Nat st k in dom S1 & k + 1 in dom S1 holds
[(S1 . k),(S1 . (k + 1))] in ReductionRel G

let k be Nat; :: thesis: ( k in dom S1 & k + 1 in dom S1 implies [(S1 . k),(S1 . (k + 1))] in ReductionRel G )
assume A15: ( k in dom S1 & k + 1 in dom S1 ) ; :: thesis: [(S1 . k),(S1 . (k + 1))] in ReductionRel G
dom S1 = dom R1 by A13, FINSEQ_3:29;
then A16: [(R1 . k),(R1 . (k + 1))] in ReductionRel G by A15, REWRITE1:def 2;
then ( R1 . k is FinSequence of FreeAtoms G & R1 . (k + 1) is FinSequence of FreeAtoms G ) by Th31;
then A17: [((R1 . k) ^ p2),((R1 . (k + 1)) ^ p2)] in ReductionRel G by A16, Th25;
( (R1 . k) ^ p2 = S1 . k & (R1 . (k + 1)) ^ p2 = S1 . (k + 1) ) by A13, A15;
hence [(S1 . k),(S1 . (k + 1))] in ReductionRel G by A17; :: thesis: verum

end;

then reconsider S1 = S1 as RedSequence of ReductionRel G by A14, REWRITE1:def 2;
1 <= len S1 by CHORD:1;
then A18: ( 1 in dom S1 & len S1 in dom S1 ) by FINSEQ_3:25;
then A19: S1 . 1 = p1 ^ p2 by A1, A13;
A20: S1 . (len S1) = q1 ^ p2 by A1, A13, A18;

per cases ( p2 = q2 or p2 <> q2 ) ;

suppose p2 = q2 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

hence ReductionRel G reduces p1 ^ p2,q1 ^ q2 by A19, A20, REWRITE1:def 3; :: thesis: verum

end;

suppose p2 <> q2 ; :: thesis: ReductionRel G reduces p1 ^ p2,q1 ^ q2

then not R2 is trivial by A2, NAT_1:23, NAT_D:60;
then reconsider R2 = R2 as FinSequence-yielding FinSequence ;
deffunc H₂( object ) -> set = q1 ^ (R2 . $1);
consider S2 being FinSequence such that
A21: ( len S2 = len R2 & ( for k being Nat st k in dom S2 holds
S2 . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A22: len S2 > 0 by A21;

now :: thesis: for k being Nat st k in dom S2 & k + 1 in dom S2 holds
[(S2 . k),(S2 . (k + 1))] in ReductionRel G

let k be Nat; :: thesis: ( k in dom S2 & k + 1 in dom S2 implies [(S2 . k),(S2 . (k + 1))] in ReductionRel G )
assume A23: ( k in dom S2 & k + 1 in dom S2 ) ; :: thesis: [(S2 . k),(S2 . (k + 1))] in ReductionRel G
dom S2 = dom R2 by A21, FINSEQ_3:29;
then A24: [(R2 . k),(R2 . (k + 1))] in ReductionRel G by A23, REWRITE1:def 2;
then ( R2 . k is FinSequence of FreeAtoms G & R2 . (k + 1) is FinSequence of FreeAtoms G ) by Th31;
then A25: [(q1 ^ (R2 . k)),(q1 ^ (R2 . (k + 1)))] in ReductionRel G by A24, Th25;
( q1 ^ (R2 . k) = S2 . k & q1 ^ (R2 . (k + 1)) = S2 . (k + 1) ) by A21, A23;
hence [(S2 . k),(S2 . (k + 1))] in ReductionRel G by A25; :: thesis: verum

end;

then reconsider S2 = S2 as RedSequence of ReductionRel G by A22, REWRITE1:def 2;
1 <= len S2 by CHORD:1;
then A26: ( 1 in dom S2 & len S2 in dom S2 ) by FINSEQ_3:25;
then A27: S2 . 1 = q1 ^ p2 by A2, A21;
A28: S2 . (len S2) = q1 ^ q2 by A2, A21, A26;
reconsider S = S1 $^ S2 as RedSequence of ReductionRel G by A20, A27, REWRITE1:8;
reconsider s = (len S2) - 1 as Nat by CHORD:1;
A29: s < (len S2) - 0 by XREAL_1:15;
(len S) + 1 = (len S1) + (len S2) by REWRITE1:66;
then A30: S . (len S) = S . ((len S1) + s)
.= S2 . (s + 1) by A29, ABCMIZ_0:33
.= q1 ^ q2 by A28 ;
1 < len S1 by A12, A13, XXREAL_0:2;
then S . 1 = p1 ^ p2 by A19, ABCMIZ_0:32;
hence ReductionRel G reduces p1 ^ p2,q1 ^ q2 by A30, REWRITE1:def 3; :: thesis: verum

end;

end;

end;

end;