let R be Relation; :: thesis: for a, b being set holds
( R reduces a,b iff R [*] reduces a,b )
let a, b be set ; :: thesis: ( R reduces a,b iff R [*] reduces a,b )
( R reduces a,b iff ( a = b or [a,b] in R [*] ) ) by Th21;
hence ( R reduces a,b implies R [*] reduces a,b ) by Th13, Th16; :: thesis: ( R [*] reduces a,b implies R reduces a,b )
given p being RedSequence of R [*] such that A1: ( a = p . 1 & b = p . (len p) ) ; :: according to REWRITE1:def 3 :: thesis: R reduces a,b
defpred S₁[ Element of NAT ] means ( $1 in dom p implies R reduces a,p . $1 );
A2: S₁[ 0 ] by Lm1;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let i be Element of 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
A4: ( i in dom p implies R reduces a,p . i ) and
A5: i + 1 in dom p ; :: thesis: R reduces a,p . (b₁ + 1)
A6: i < len p by A5, 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, Th13; :: thesis: verum

end;

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

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

end;

end;

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

A8: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A2, A3);
len p in dom p by FINSEQ_5:6;
hence R reduces a,b by A1, A8; :: thesis: verum