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 )
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;
assume A2: j in dom p ; :: thesis: ( not i <= j or p . i <= p . j )
A3: 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 A4: 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 )
reconsider l = i + k as Element of NAT ;
A5: 0 <= k by NAT_1:2;
assume j = i + (k + 1) ; :: thesis: ( not i in dom p or not j in dom p or p . i <= p . j )
then A6: j = l + 1 ;
assume A7: i in dom p ; :: thesis: ( not j in dom p or p . i <= p . j )
then 1 <= i by FINSEQ_3:27;
then A8: 1 + 0 <= l by A5, XREAL_1:9;
assume A9: j in dom p ; :: thesis: p . i <= p . j
then j <= len p by FINSEQ_3:27;
then l < len p by A6, NAT_1:13;
then A10: l in dom p by A8, FINSEQ_3:27;
then A11: p . i <= p . l by A4, A7;
p . l <= p . j by A9, A6, A10, Def1;
hence p . i <= p . j by A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

A12: S₁[ 0 ] ;
A13: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A12, A3);
assume i <= j ; :: thesis: p . i <= p . j
then consider n being Nat such that
A14: j = i + n by NAT_1:10;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
j = i + n by A14;
hence p . i <= p . j by A1, A2, A13; :: thesis: verum