let R be Relation; for p being RedSequence of R
for i, j being 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; for i, j being Nat st i in dom p & j in dom p & i <= j holds
R reduces p . i,p . j
let i, j be Nat; ( i in dom p & j in dom p & i <= j implies R reduces p . i,p . j )
defpred S1[ 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
; R reduces p . i,p . j
consider k being Nat such that
A4:
j = i + k
by A3, NAT_1:10;
now for j being Nat st ( i + j in dom p implies R reduces p . i,p . (i + j) ) & i + (j + 1) in dom p holds
R reduces p . i,p . (i + (j + 1))A5:
i >= 1
by A1, Lm1;
let j be
Nat;
( ( 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
;
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 Th15;
hence
R reduces p . i,
p . (i + (j + 1))
by A6, A5, A9, Lm3, Th16;
verum end;
then A10:
for k being Nat st S1[k] holds
S1[k + 1]
;
A11:
S1[ 0 ]
by Th12;
A12:
for j being Nat holds S1[j]
from NAT_1:sch 2(A11, A10);
thus
R reduces p . i,p . j
by A2, A12, A4; verum