let p be non-decreasing FinSequence of REAL ; :: thesis: for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds
p . i <= p . j
let i, j be Element of NAT ; :: thesis: ( i in dom p & j in dom p & i <= j implies p . i <= p . j )
assume A1: i in dom p ; :: thesis: ( not j in dom p or not i <= j or p . i <= p . j )
assume A2: j in dom p ; :: thesis: ( not i <= j or p . i <= p . j )
assume i <= j ; :: thesis: p . i <= p . j
then consider n being Nat such that
A3: j = i + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A4: j = i + n by A3;
defpred S₁[ Element of NAT ] means for i, j being Element of NAT st j = i + $1 & i in dom p & j in dom p holds
p . i <= p . j;
A5: S₁[ 0 ] ;
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let i, j be Element of NAT ; :: thesis: ( j = i + (k + 1) & i in dom p & j in dom p implies p . i <= p . j )
assume A8: j = i + (k + 1) ; :: thesis: ( not i in dom p or not j in dom p or p . i <= p . j )
assume A9: i in dom p ; :: thesis: ( not j in dom p or p . i <= p . j )
assume A10: j in dom p ; :: thesis: p . i <= p . j
reconsider l = i + k as Element of NAT ;
A11: j = l + 1 by A8;
( 1 <= i & 0 <= k ) by A9, FINSEQ_3:27, NAT_1:2;
then A12: 1 + 0 <= l by XREAL_1:9;
j <= len p by A10, FINSEQ_3:27;
then l < len p by A11, NAT_1:13;
then A13: l in dom p by A12, FINSEQ_3:27;
then A14: p . i <= p . l by A7, A9;
p . l <= p . j by A10, A11, A13, Def1;
hence p . i <= p . j by A14, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A6);
hence p . i <= p . j by A1, A2, A4; :: thesis: verum