let p be real-valued FinSequence; :: thesis: ( ( for n being Nat st n in dom p & n + 1 in dom p holds
p . n <= p . (n + 1) ) implies for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j )
assume A0: for n being Nat st n in dom p & n + 1 in dom p holds
p . n <= p . (n + 1) ; :: thesis: for i, j being Nat st i in dom p & j in dom p & i <= j holds
p . i <= p . j
let i, j be 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₁[ Nat] means for i, j being 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 Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let i, j be Nat; :: thesis: ( j = i + (k + 1) & i in dom p & j in dom p implies p . i <= p . j )
reconsider l = i + k as Nat ;
assume j = i + (k + 1) ; :: thesis: ( not i in dom p or not j in dom p or p . i <= p . j )
then A5: j = l + 1 ;
assume A6: i in dom p ; :: thesis: ( not j in dom p or p . i <= p . j )
then 1 <= i by FINSEQ_3:25;
then A7: 1 + 0 <= l by XREAL_1:7;
assume A8: j in dom p ; :: thesis: p . i <= p . j
then j <= len p by FINSEQ_3:25;
then l < len p by A5, NAT_1:13;
then A9: l in dom p by A7, FINSEQ_3:25;
then A10: p . i <= p . l by A4, A6;
p . l <= p . j by A0, A8, A5, A9;
hence p . i <= p . j by A10, XXREAL_0:2; :: thesis: verum

end;

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

end;

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