let p be FinSequence of REAL ; :: 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_{1}[ 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_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A12: for k being Nat holds S_{1}[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

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

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

S

proof

A11:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

S_{1}[k + 1]
_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

S

proof

hence
S
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;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

A12: for k being Nat holds S

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