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

defpred S₁[ Element of 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:27;
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

( 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:8;
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;

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

end;

i + 1 <= j by A4, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:235;
then A12: i + (1 + (j -' (i + 1))) = j ;
A13: f /. i = f . i by A2, PARTFUN1:def 8;
A14: j <= len f by A3, FINSEQ_3:27;
then i < len f by A4, XXREAL_0:2;
then A15: S₁[ 0 ] by A1, A5;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A15, A6);
then f /. i < f /. j by A14, A12;
hence f . i < f . j by A3, A13, 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