now :: thesis: for a, b, c being object st [a,b] in ReductionRel H & [a,c] in ReductionRel H holds
b,c are_convergent<=1_wrt ReductionRel H

set R = ReductionRel H;
set C = the carrier of ((FreeAtoms H) *+^+<0>);
let a, b, c be object ; :: thesis: ( [a,b] in ReductionRel H & [a,c] in ReductionRel H implies b,c are_convergent<=1_wrt ReductionRel H )
assume A1: ( [a,b] in ReductionRel H & [a,c] in ReductionRel H ) ; :: thesis: b,c are_convergent<=1_wrt ReductionRel H
A2: field (ReductionRel H) c= the carrier of ((FreeAtoms H) *+^+<0>) \/ the carrier of ((FreeAtoms H) *+^+<0>) by RELSET_1:8;
( a in field (ReductionRel H) & b in field (ReductionRel H) & c in field (ReductionRel H) ) by A1, RELAT_1:15;
then ( a in the carrier of ((FreeAtoms H) *+^+<0>) & b in the carrier of ((FreeAtoms H) *+^+<0>) & c in the carrier of ((FreeAtoms H) *+^+<0>) ) by A2;
then ( a in (FreeAtoms H) * & b in (FreeAtoms H) * & c in (FreeAtoms H) * ) by MONOID_0:61;
then reconsider p = a, q1 = b, q2 = c as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

proof

per cases ( b = c or ex s, t being FinSequence of FreeAtoms H ex i being Element of I ex f, g, h being Element of (H . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) or ex r, s, t being FinSequence of FreeAtoms H ex i, j being Element of I st
( ( p = (((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ex g, h being Element of (H . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ) ) by A1, Th39;

suppose b = c ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

hence ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) ) ; :: thesis: verum

end;

suppose ex s, t being FinSequence of FreeAtoms H ex i being Element of I ex f, g, h being Element of (H . i) st
( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

then consider s, t being FinSequence of FreeAtoms H, i being Element of I, f, g, h being Element of (H . i) such that
A3: ( p = (s ^ <*[i,f],[i,g],[i,h]*>) ^ t & ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) ) ;
reconsider v = <*[i,((f * g) * h)]*> as FinSequence of FreeAtoms H by Th23;
A4: v = <*[i,(f * (g * h))]*> by GROUP_1:def 3;
take (s ^ v) ^ t ; :: thesis: ( ( [b,((s ^ v) ^ t)] in ReductionRel H or b = (s ^ v) ^ t ) & ( [c,((s ^ v) ^ t)] in ReductionRel H or c = (s ^ v) ^ t ) )

per cases ( ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) or ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ) by A3;

suppose ( q1 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t & q2 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t ) ; :: thesis: ( ( [b,((s ^ v) ^ t)] in ReductionRel H or b = (s ^ v) ^ t ) & ( [c,((s ^ v) ^ t)] in ReductionRel H or c = (s ^ v) ^ t ) )

hence ( ( [b,((s ^ v) ^ t)] in ReductionRel H or b = (s ^ v) ^ t ) & ( [c,((s ^ v) ^ t)] in ReductionRel H or c = (s ^ v) ^ t ) ) by A4, Th26; :: thesis: verum

end;

suppose ( q1 = (s ^ <*[i,f],[i,(g * h)]*>) ^ t & q2 = (s ^ <*[i,(f * g)],[i,h]*>) ^ t ) ; :: thesis: ( ( [b,((s ^ v) ^ t)] in ReductionRel H or b = (s ^ v) ^ t ) & ( [c,((s ^ v) ^ t)] in ReductionRel H or c = (s ^ v) ^ t ) )

hence ( ( [b,((s ^ v) ^ t)] in ReductionRel H or b = (s ^ v) ^ t ) & ( [c,((s ^ v) ^ t)] in ReductionRel H or c = (s ^ v) ^ t ) ) by A4, Th26; :: thesis: verum

end;

end;

end;

suppose ex r, s, t being FinSequence of FreeAtoms H ex i, j being Element of I st
( ( p = (((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ex g, h being Element of (H . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

then consider r, s, t being FinSequence of FreeAtoms H, i, j being Element of I such that
A5: ( ( p = (((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ex g, h being Element of (H . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ) ;

per cases ( ( p = (((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ex g, h being Element of (H . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ) by A5;

suppose A6: ( p = (((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

take (r ^ s) ^ t ; :: thesis: ( ( [b,((r ^ s) ^ t)] in ReductionRel H or b = (r ^ s) ^ t ) & ( [c,((r ^ s) ^ t)] in ReductionRel H or c = (r ^ s) ^ t ) )

per cases ( ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) by A6;

suppose A7: ( q1 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t ) ; :: thesis: ( ( [b,((r ^ s) ^ t)] in ReductionRel H or b = (r ^ s) ^ t ) & ( [c,((r ^ s) ^ t)] in ReductionRel H or c = (r ^ s) ^ t ) )

then q2 = (r ^ <*[i,(1_ (H . i))]*>) ^ (s ^ t) by FINSEQ_1:32;
then ( [q1,((r ^ s) ^ t)] in ReductionRel H & [q2,(r ^ (s ^ t))] in ReductionRel H ) by A7, Th28;
hence ( ( [b,((r ^ s) ^ t)] in ReductionRel H or b = (r ^ s) ^ t ) & ( [c,((r ^ s) ^ t)] in ReductionRel H or c = (r ^ s) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

suppose A8: ( q1 = ((r ^ <*[i,(1_ (H . i))]*>) ^ s) ^ t & q2 = ((r ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ; :: thesis: ( ( [b,((r ^ s) ^ t)] in ReductionRel H or b = (r ^ s) ^ t ) & ( [c,((r ^ s) ^ t)] in ReductionRel H or c = (r ^ s) ^ t ) )

then q1 = (r ^ <*[i,(1_ (H . i))]*>) ^ (s ^ t) by FINSEQ_1:32;
then ( [q1,(r ^ (s ^ t))] in ReductionRel H & [q2,((r ^ s) ^ t)] in ReductionRel H ) by A8, Th28;
hence ( ( [b,((r ^ s) ^ t)] in ReductionRel H or b = (r ^ s) ^ t ) & ( [c,((r ^ s) ^ t)] in ReductionRel H or c = (r ^ s) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

end;

end;

suppose ex g, h being Element of (H . i) st
( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

then consider g, h being Element of (H . i) such that
A9: ( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) ;
reconsider v = <*[i,(g * h)]*> as FinSequence of FreeAtoms H by Th23;

per cases ( ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) or ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) or ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ) by A9;

suppose A10: ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

take ((r ^ v) ^ s) ^ t ; :: thesis: ( ( [b,(((r ^ v) ^ s) ^ t)] in ReductionRel H or b = ((r ^ v) ^ s) ^ t ) & ( [c,(((r ^ v) ^ s) ^ t)] in ReductionRel H or c = ((r ^ v) ^ s) ^ t ) )

per cases ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) or ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ) by A10;

suppose A11: ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t & q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t ) ; :: thesis: ( ( [b,(((r ^ v) ^ s) ^ t)] in ReductionRel H or b = ((r ^ v) ^ s) ^ t ) & ( [c,(((r ^ v) ^ s) ^ t)] in ReductionRel H or c = ((r ^ v) ^ s) ^ t ) )

then q2 = (r ^ <*[i,g],[i,h]*>) ^ (s ^ t) by FINSEQ_1:32;
then ( [q2,((r ^ v) ^ (s ^ t))] in ReductionRel H & [q1,(((r ^ v) ^ s) ^ t)] in ReductionRel H ) by A11, Th26, Th28;
hence ( ( [b,(((r ^ v) ^ s) ^ t)] in ReductionRel H or b = ((r ^ v) ^ s) ^ t ) & ( [c,(((r ^ v) ^ s) ^ t)] in ReductionRel H or c = ((r ^ v) ^ s) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

suppose A12: ( q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,(1_ (H . j))]*>) ^ t ) ; :: thesis: ( ( [b,(((r ^ v) ^ s) ^ t)] in ReductionRel H or b = ((r ^ v) ^ s) ^ t ) & ( [c,(((r ^ v) ^ s) ^ t)] in ReductionRel H or c = ((r ^ v) ^ s) ^ t ) )

then q1 = (r ^ <*[i,g],[i,h]*>) ^ (s ^ t) by FINSEQ_1:32;
then ( [q1,((r ^ v) ^ (s ^ t))] in ReductionRel H & [q2,(((r ^ v) ^ s) ^ t)] in ReductionRel H ) by A12, Th26, Th28;
hence ( ( [b,(((r ^ v) ^ s) ^ t)] in ReductionRel H or b = ((r ^ v) ^ s) ^ t ) & ( [c,(((r ^ v) ^ s) ^ t)] in ReductionRel H or c = ((r ^ v) ^ s) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

end;

end;

suppose A13: ( p = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,g],[i,h]*>) ^ t & ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

take ((r ^ s) ^ v) ^ t ; :: thesis: ( ( [b,(((r ^ s) ^ v) ^ t)] in ReductionRel H or b = ((r ^ s) ^ v) ^ t ) & ( [c,(((r ^ s) ^ v) ^ t)] in ReductionRel H or c = ((r ^ s) ^ v) ^ t ) )

per cases ( ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) or ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ) by A13;

suppose A14: ( q1 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t & q2 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t ) ; :: thesis: ( ( [b,(((r ^ s) ^ v) ^ t)] in ReductionRel H or b = ((r ^ s) ^ v) ^ t ) & ( [c,(((r ^ s) ^ v) ^ t)] in ReductionRel H or c = ((r ^ s) ^ v) ^ t ) )

then q1 = ((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ (v ^ t) by FINSEQ_1:32
.= (r ^ <*[j,(1_ (H . j))]*>) ^ (s ^ (v ^ t)) by FINSEQ_1:32 ;
then ( [q1,(r ^ (s ^ (v ^ t)))] in ReductionRel H & [q2,(((r ^ s) ^ v) ^ t)] in ReductionRel H ) by A14, Th26, Th28;
then ( [q1,((r ^ s) ^ (v ^ t))] in ReductionRel H & [q2,(((r ^ s) ^ v) ^ t)] in ReductionRel H ) by FINSEQ_1:32;
hence ( ( [b,(((r ^ s) ^ v) ^ t)] in ReductionRel H or b = ((r ^ s) ^ v) ^ t ) & ( [c,(((r ^ s) ^ v) ^ t)] in ReductionRel H or c = ((r ^ s) ^ v) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

suppose A15: ( q1 = ((r ^ s) ^ <*[i,g],[i,h]*>) ^ t & q2 = (((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ <*[i,(g * h)]*>) ^ t ) ; :: thesis: ( ( [b,(((r ^ s) ^ v) ^ t)] in ReductionRel H or b = ((r ^ s) ^ v) ^ t ) & ( [c,(((r ^ s) ^ v) ^ t)] in ReductionRel H or c = ((r ^ s) ^ v) ^ t ) )

then q2 = ((r ^ <*[j,(1_ (H . j))]*>) ^ s) ^ (v ^ t) by FINSEQ_1:32
.= (r ^ <*[j,(1_ (H . j))]*>) ^ (s ^ (v ^ t)) by FINSEQ_1:32 ;
then ( [q2,(r ^ (s ^ (v ^ t)))] in ReductionRel H & [q1,(((r ^ s) ^ v) ^ t)] in ReductionRel H ) by A15, Th26, Th28;
then ( [q2,((r ^ s) ^ (v ^ t))] in ReductionRel H & [q1,(((r ^ s) ^ v) ^ t)] in ReductionRel H ) by FINSEQ_1:32;
hence ( ( [b,(((r ^ s) ^ v) ^ t)] in ReductionRel H or b = ((r ^ s) ^ v) ^ t ) & ( [c,(((r ^ s) ^ v) ^ t)] in ReductionRel H or c = ((r ^ s) ^ v) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

end;

end;

suppose ex g9, h9 being Element of (H . j) st
( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ; :: thesis: ex d being object st
( ( [b,d] in ReductionRel H or b = d ) & ( [c,d] in ReductionRel H or c = d ) )

then consider g9, h9 being Element of (H . j) such that
A16: ( p = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & ( ( q1 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ <*[j,(g9 * h9)]*>) ^ t & q2 = (((r ^ <*[i,(g * h)]*>) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) ) ;
reconsider w = <*[j,(g9 * h9)]*> as FinSequence of FreeAtoms H by Th23;
take (((r ^ v) ^ s) ^ w) ^ t ; :: thesis: ( ( [b,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or b = (((r ^ v) ^ s) ^ w) ^ t ) & ( [c,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or c = (((r ^ v) ^ s) ^ w) ^ t ) )

per cases ( ( q1 = (((r ^ v) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ w) ^ t ) or ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ w) ^ t & q2 = (((r ^ v) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ) by A16;

suppose A17: ( q1 = (((r ^ v) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t & q2 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ w) ^ t ) ; :: thesis: ( ( [b,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or b = (((r ^ v) ^ s) ^ w) ^ t ) & ( [c,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or c = (((r ^ v) ^ s) ^ w) ^ t ) )

then q2 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ (w ^ t) by FINSEQ_1:32
.= (r ^ <*[i,g],[i,h]*>) ^ (s ^ (w ^ t)) by FINSEQ_1:32 ;
then ( [q2,((r ^ v) ^ (s ^ (w ^ t)))] in ReductionRel H & [q1,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H ) by A17, Th26;
then ( [q2,(((r ^ v) ^ s) ^ (w ^ t))] in ReductionRel H & [q1,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H ) by FINSEQ_1:32;
hence ( ( [b,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or b = (((r ^ v) ^ s) ^ w) ^ t ) & ( [c,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or c = (((r ^ v) ^ s) ^ w) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

suppose A18: ( q1 = (((r ^ <*[i,g],[i,h]*>) ^ s) ^ w) ^ t & q2 = (((r ^ v) ^ s) ^ <*[j,g9],[j,h9]*>) ^ t ) ; :: thesis: ( ( [b,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or b = (((r ^ v) ^ s) ^ w) ^ t ) & ( [c,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or c = (((r ^ v) ^ s) ^ w) ^ t ) )

then q1 = ((r ^ <*[i,g],[i,h]*>) ^ s) ^ (w ^ t) by FINSEQ_1:32
.= (r ^ <*[i,g],[i,h]*>) ^ (s ^ (w ^ t)) by FINSEQ_1:32 ;
then ( [q1,((r ^ v) ^ (s ^ (w ^ t)))] in ReductionRel H & [q2,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H ) by A18, Th26;
then ( [q1,(((r ^ v) ^ s) ^ (w ^ t))] in ReductionRel H & [q2,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H ) by FINSEQ_1:32;
hence ( ( [b,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or b = (((r ^ v) ^ s) ^ w) ^ t ) & ( [c,((((r ^ v) ^ s) ^ w) ^ t)] in ReductionRel H or c = (((r ^ v) ^ s) ^ w) ^ t ) ) by FINSEQ_1:32; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

hence b,c are_convergent<=1_wrt ReductionRel H by REWRITE1:def 9; :: thesis: verum

end;

hence ReductionRel H is subcommutative by REWRITE1:def 21; :: thesis: verum