let f be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ) implies f is increasing )
assume A1: for k being Element of NAT st 1 <= k & k < len f holds
f /. k < f /. (k + 1) ; :: thesis: f is increasing

now

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

now

assume A2: ( i in dom f & j in dom f & i < j ) ; :: thesis: f . i < f . j
then A3: ( 1 <= i & i <= len f ) by FINSEQ_3:27;
defpred S₁[ Element of NAT ] means ( i + (1 + $1) <= len f implies f /. i < f /. (i + (1 + $1)) );
A4: ( 1 <= j & j <= len f ) by A2, FINSEQ_3:27;
then i < len f by A2, XXREAL_0:2;
then A5: S₁[ 0 ] by A1, A3;
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: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; :: thesis: S₁[k + 1]

now

assume A8: i + (1 + (k + 1)) <= len f ; :: thesis: f /. i < f /. (i + (1 + (k + 1)))
A9: 1 <= i + 1 by NAT_1:11;
i + 1 <= (i + 1) + k by NAT_1:11;
then A10: 1 <= (i + 1) + k by A9, XXREAL_0:2;
1 + k < 1 + (k + 1) by NAT_1:13;
then A11: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:8;
then A12: i + (1 + k) < len f by A8, XXREAL_0:2;
i + (1 + (k + 1)) = (i + (1 + k)) + 1 ;
then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A10, A12;
hence f /. i < f /. (i + (1 + (k + 1))) by A7, A8, A11, XXREAL_0:2; :: thesis: verum

end;

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

end;

A13: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A6);
i + 1 <= j by A2, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:235;
then i + (1 + (j -' (i + 1))) = j ;
then A14: f /. i < f /. j by A4, A13;
f /. i = f . i by A2, PARTFUN1:def 8;
hence f . i < f . j by A2, A14, PARTFUN1:def 8; :: thesis: verum

end;

hence ( i in dom f & j in dom f & i < j implies f . i < f . j ) ; :: thesis: verum

end;

hence f is increasing by SEQM_3:def 1; :: thesis: verum