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 S1[ 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 . (b1 + 1) )
assume A3: ( i in dom p implies R reduces a,p . i ) ; :: thesis: ( i + 1 in dom p implies R reduces a,p . (b1 + 1) )
assume A4: i + 1 in dom p ; :: thesis: R reduces a,p . (b1 + 1)
per cases ( i in dom p or not i in dom p ) ;
suppose A5: i in dom p ; :: thesis: R reduces a,p . (b1 + 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 . (b1 + 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 S1[k] holds
S1[k + 1] ;
A7: len p in dom p by Lm3;
A8: S1[ 0 ] by Lm1;
for i being Nat holds S1[i] from NAT_1:sch 2(A8, A6);
 hence R reduces a,b by A2, A7; :: thesis: verum