let R be Relation; :: thesis: for a, b being object holds
( R reduces a,b iff R [*] reduces a,b )
let a, b be object ; :: thesis: ( R reduces a,b iff R [*] reduces a,b )
( R reduces a,b iff ( a = b or [a,b] in R [*] ) ) by Th20;
hence ( R reduces a,b implies R [*] reduces a,b ) by Th12, Th15; :: thesis: ( R [*] reduces a,b implies R reduces a,b )
given p being RedSequence of R [*] such that A1: a = p . 1 and
A2: b = p . (len p) ; :: according to REWRITE1:def 3 :: thesis: R reduces a,b
defpred S₁[ Nat] means ( $1 in dom p implies R reduces a,p . $1 );

now :: thesis: for i being Nat st ( i in dom p implies R reduces a,p . i ) & i + 1 in dom p holds
R reduces a,p . (i + 1)

let i be Nat; :: thesis: ( ( i in dom p implies R reduces a,p . i ) & i + 1 in dom p implies R reduces a,p . (b₁ + 1) )
assume that
A3: ( i in dom p implies R reduces a,p . i ) and
A4: i + 1 in dom p ; :: thesis: R reduces a,p . (b₁ + 1)
A5: i < len p by A4, Lm2;

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

suppose i = 0 ; :: thesis: R reduces a,p . (b₁ + 1)

hence R reduces a,p . (i + 1) by A1, Th12; :: thesis: verum

end;

suppose A6: i > 0 ; :: thesis: R reduces a,p . (b₁ + 1)

then i in dom p by A5, Lm3;
then [(p . i),(p . (i + 1))] in R [*] by A4, Def2;
then R reduces p . i,p . (i + 1) by Th20;
hence R reduces a,p . (i + 1) by A3, A5, A6, Lm3, Th16; :: thesis: verum

end;

end;

end;

then A7: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A8: len p in dom p by FINSEQ_5:6;
A9: S₁[ 0 ] by Lm1;
for i being Nat holds S₁[i] from NAT_1:sch 2(A9, A7);
hence R reduces a,b by A2, A8; :: thesis: verum