let f be FinSequence of REAL ; :: thesis: ( ( for k being Nat st 1 <= k & k < len f holds

f /. k < f /. (k + 1) ) implies f is increasing )

assume A1: for k being Nat st 1 <= k & k < len f holds

f /. k < f /. (k + 1) ; :: thesis: f is increasing

f /. k < f /. (k + 1) ) implies f is increasing )

assume A1: for k being Nat st 1 <= k & k < len f holds

f /. k < f /. (k + 1) ; :: thesis: f is increasing

now :: thesis: for i, j being Nat st i in dom f & j in dom f & i < j holds

f . i < f . j

hence
f is increasing
by SEQM_3:def 1; :: thesis: verumf . i < f . j

let i, j be Nat; :: thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )

end;now :: thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j )

hence
( i in dom f & j in dom f & i < j implies f . i < f . j )
; :: thesis: verumdefpred S_{1}[ Nat] means ( i + (1 + $1) <= len f implies f /. i < f /. (i + (1 + $1)) );

assume that

A2: i in dom f and

A3: j in dom f and

A4: i < j ; :: thesis: f . i < f . j

A5: 1 <= i by A2, FINSEQ_3:25;

A6: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then j -' (i + 1) = j - (i + 1) by XREAL_1:233;

then A12: i + (1 + (j -' (i + 1))) = j ;

A13: f /. i = f . i by A2, PARTFUN1:def 6;

A14: j <= len f by A3, FINSEQ_3:25;

then i < len f by A4, XXREAL_0:2;

then A15: S_{1}[ 0 ]
by A1, A5;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A15, A6);

then f /. i < f /. j by A14, A12;

hence f . i < f . j by A3, A13, PARTFUN1:def 6; :: thesis: verum

end;assume that

A2: i in dom f and

A3: j in dom f and

A4: i < j ; :: thesis: f . i < f . j

A5: 1 <= i by A2, FINSEQ_3:25;

A6: for k being Nat st S

S

proof

i + 1 <= j
by A4, NAT_1:13;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; :: thesis: S_{1}[k + 1]

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

end;assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; :: thesis: S

now :: thesis: ( i + (1 + (k + 1)) <= len f implies f /. i < f /. (i + (1 + (k + 1))) )

hence
S
( 1 <= i + 1 & i + 1 <= (i + 1) + k )
by NAT_1:11;

then A8: 1 <= (i + 1) + k by XXREAL_0:2;

A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;

1 + k < 1 + (k + 1) by NAT_1:13;

then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6;

assume A11: i + (1 + (k + 1)) <= len f ; :: thesis: f /. i < f /. (i + (1 + (k + 1)))

then i + (1 + k) < len f by A10, XXREAL_0:2;

then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9;

hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; :: thesis: verum

end;then A8: 1 <= (i + 1) + k by XXREAL_0:2;

A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;

1 + k < 1 + (k + 1) by NAT_1:13;

then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6;

assume A11: i + (1 + (k + 1)) <= len f ; :: thesis: f /. i < f /. (i + (1 + (k + 1)))

then i + (1 + k) < len f by A10, XXREAL_0:2;

then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9;

hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; :: thesis: verum

then j -' (i + 1) = j - (i + 1) by XREAL_1:233;

then A12: i + (1 + (j -' (i + 1))) = j ;

A13: f /. i = f . i by A2, PARTFUN1:def 6;

A14: j <= len f by A3, FINSEQ_3:25;

then i < len f by A4, XXREAL_0:2;

then A15: S

for k being Nat holds S

then f /. i < f /. j by A14, A12;

hence f . i < f . j by A3, A13, PARTFUN1:def 6; :: thesis: verum