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 S1[ 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 S1[i] ) & i + 1 in dom p holds
S1[i + 1]
let i be Nat; :: thesis: ( ( i in dom p implies S1[i] ) & i + 1 in dom p implies S1[b1 + 1] )
assume that
A5: ( i in dom p implies S1[i] ) and
A6: i + 1 in dom p ; :: thesis: S1[b1 + 1]
per cases ( i = 0 or i > 0 ) ;
suppose A7: i = 0 ; :: thesis: S1[b1 + 1]
R reduces c,c by Th12;
hence S1[i + 1] by A2, A4, A7; :: thesis: verum
end;
suppose A8: i > 0 ; :: thesis: S1[b1 + 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 S1[i + 1] by A10, A13; :: thesis: verum
end;
end;
end;
then A16: for k being Nat st S1[k] holds
S1[k + 1] ;
A17: len p in dom p by FINSEQ_5:6;
A18: S1[ 0 ] by Lm1;
for i being Nat holds S1[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