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 that
A1: i in dom p and
A2: j in dom p and
A3: i <= j ; :: thesis: R reduces p . i,p . j
consider k being Nat such that
A4: j = i + k by A3, NAT_1:10;

now

A5: i >= 1 by A1, Lm1;
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
A6: ( i + j in dom p implies R reduces p . i,p . (i + j) ) and
A7: i + (j + 1) in dom p ; :: thesis: R reduces p . i,p . (i + (j + 1))
A8: i + (j + 1) = (i + j) + 1 ;
then A9: i + j < len p by A7, Lm2;
then i + j in dom p by A5, Lm3;
then [(p . (i + j)),(p . (i + (j + 1)))] in R by A7, A8, Def2;
then R reduces p . (i + j),p . (i + (j + 1)) by Th16;
hence R reduces p . i,p . (i + (j + 1)) by A6, A5, A9, Lm3, Th17; :: thesis: verum

end;

then A10: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A11: S₁[ 0 ] by Th13;
A12: for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A11, A10);
k in NAT by ORDINAL1:def 13;
hence R reduces p . i,p . j by A2, A12, A4; :: thesis: verum