let R be Relation; :: thesis: ( R is subcommutative implies for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R )
assume A1: R is subcommutative ; :: thesis: for a, b, c being object st R reduces a,b & [a,c] in R holds
b,c are_convergent_wrt R
let a, b, c be object ; :: thesis: ( R reduces a,b & [a,c] in R implies b,c are_convergent_wrt R )
given p being RedSequence of R such that A2: p . 1 = a and
A3: p . (len p) = b ; :: according to REWRITE1:def 3 :: thesis: ( not [a,c] in R or b,c are_convergent_wrt R )
defpred S₁[ Nat] means ( $1 in dom p implies ex d being object st
( ( [(p . $1),d] in R or p . $1 = d ) & R reduces c,d ) );
assume A4: [a,c] in R ; :: thesis: b,c are_convergent_wrt R

now :: thesis: for i being Nat st ( i in dom p implies S₁[i] ) & i + 1 in dom p holds
S₁[i + 1]

let i be Nat; :: thesis: ( ( i in dom p implies S₁[i] ) & i + 1 in dom p implies S₁[b₁ + 1] )
assume that
A5: ( i in dom p implies S₁[i] ) and
A6: i + 1 in dom p ; :: thesis: S₁[b₁ + 1]

per cases ( i = 0 or i > 0 ) ;

suppose A7: i = 0 ; :: thesis: S₁[b₁ + 1]

R reduces c,c by Th12;
hence S₁[i + 1] by A2, A4, A7; :: thesis: verum

end;

suppose A8: i > 0 ; :: thesis: S₁[b₁ + 1]

A9: i < len p by A6, Lm2;
then consider d being object such that
A10: ( [(p . i),d] in R or p . i = d ) and
A11: R reduces c,d by A5, A8, Lm3;
i in dom p by A8, A9, Lm3;
then A12: [(p . i),(p . (i + 1))] in R by A6, Def2;

A13: now :: thesis: ( [(p . i),d] in R implies ex e being object st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e ) )

assume [(p . i),d] in R ; :: thesis: ex e being object st
( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
then p . (i + 1),d are_convergent<=1_wrt R by A1, A12;
then consider e being object such that
A14: ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) and
A15: ( [d,e] in R or d = e ) ;
take e = e; :: thesis: ( ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) & R reduces c,e )
thus ( [(p . (i + 1)),e] in R or p . (i + 1) = e ) by A14; :: thesis: R reduces c,e
R reduces d,e by A15, Th12, Th15;
hence R reduces c,e by A11, Th16; :: thesis: verum

end;

now :: thesis: ( p . i = d implies R reduces c,p . (i + 1) )

assume p . i = d ; :: thesis: R reduces c,p . (i + 1)
then R reduces d,p . (i + 1) by A12, Th15;
hence R reduces c,p . (i + 1) by A11, Th16; :: thesis: verum

end;

hence S₁[i + 1] by A10, A13; :: thesis: verum

end;

end;

end;

then A16: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A17: len p in dom p by FINSEQ_5:6;
A18: S₁[ 0 ] by Lm1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A18, A16);
then consider d being object such that
A19: ( ( [b,d] in R or b = d ) & R reduces c,d ) by A3, A17;
take d ; :: according to REWRITE1:def 7 :: thesis: ( R reduces b,d & R reduces c,d )
thus ( R reduces b,d & R reduces c,d ) by A19, Th12, Th15; :: thesis: verum