let R be Relation; :: thesis: for X being set
for a, b being object holds
( R reduces a,b iff R \/ (id X) reduces a,b )
let X be set ; :: thesis: for a, b being object holds
( R reduces a,b iff R \/ (id X) reduces a,b )
let a, b be object ; :: thesis: ( R reduces a,b iff R \/ (id X) reduces a,b )
thus ( R reduces a,b implies R \/ (id X) reduces a,b ) by Th22, XBOOLE_1:7; :: thesis: ( R \/ (id X) reduces a,b implies R reduces a,b )
given p being RedSequence of R \/ (id X) such that A1: p . 1 = a and
A2: p . (len p) = b ; :: 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 A3: ( i in dom p implies R reduces a,p . i ) ; :: thesis: ( i + 1 in dom p implies R reduces a,p . (b₁ + 1) )
assume A4: i + 1 in dom p ; :: thesis: R reduces a,p . (b₁ + 1)

per cases ( i in dom p or not i in dom p ) ;

suppose A5: i in dom p ; :: thesis: R reduces a,p . (b₁ + 1)

then [(p . i),(p . (i + 1))] in R \/ (id X) by A4, Def2;
then ( [(p . i),(p . (i + 1))] in R or [(p . i),(p . (i + 1))] in id X ) by XBOOLE_0:def 3;
then ( R reduces p . i,p . (i + 1) or p . i = p . (i + 1) ) by Th15, RELAT_1:def 10;
hence R reduces a,p . (i + 1) by A3, A5, Th16; :: thesis: verum

end;

suppose not i in dom p ; :: thesis: R reduces a,p . (b₁ + 1)

then ( i < 0 + 1 or ( i > len p & i + 1 <= len p ) ) by A4, Lm1, Lm3;
then i = 0 by NAT_1:13;
hence R reduces a,p . (i + 1) by A1, Th12; :: thesis: verum

end;

end;

end;

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