let R be Relation; :: thesis: for p being RedSequence of R
for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
let p be RedSequence of R; :: thesis: for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
let i, j be Element of NAT ; :: thesis: ( i in dom p & j in dom p & i <= j implies R reduces p . i,p . j )
defpred S₁[ Element of NAT ] means ( i + $1 in dom p implies R reduces p . i,p . (i + $1) );
assume A1: ( i in dom p & j in dom p & i <= j ) ; :: thesis: R reduces p . i,p . j
A2: S₁[ 0 ] by Th13;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

let j be Element of NAT ; :: thesis: ( ( i + j in dom p implies R reduces p . i,p . (i + j) ) & i + (j + 1) in dom p implies R reduces p . i,p . (i + (j + 1)) )
assume that
A4: ( i + j in dom p implies R reduces p . i,p . (i + j) ) and
A5: i + (j + 1) in dom p ; :: thesis: R reduces p . i,p . (i + (j + 1))
A6: i + (j + 1) = (i + j) + 1 ;
( i <= i + j & i >= 1 ) by A1, Lm1, NAT_1:11;
then A7: ( i + j >= 1 & i + j < len p ) by A5, A6, Lm2, XXREAL_0:2;
then i + j in dom p by Lm3;
then [(p . (i + j)),(p . (i + (j + 1)))] in R by A5, A6, Def2;
then ( R reduces p . i,p . (i + j) & R reduces p . (i + j),p . (i + (j + 1)) ) by A4, A7, Lm3, Th16;
hence R reduces p . i,p . (i + (j + 1)) by Th17; :: thesis: verum

end;

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

end;

A8: for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A2, A3);
consider k being Nat such that
A9: j = i + k by A1, NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence R reduces p . i,p . j by A1, A8, A9; :: thesis: verum