hereby :: thesis: ( ( for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) ) implies h is increasing )

assume A1: h is increasing ; :: thesis: for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1)
let i be Nat; :: thesis: ( 1 <= i & i < len h implies h . i < h . (i + 1) )
assume that
A2: 1 <= i and
A3: i < len h ; :: thesis: h . i < h . (i + 1)
( 1 <= i + 1 & i + 1 <= len h ) by A3, NAT_1:12, NAT_1:13;
then A4: ( i in dom h & i + 1 in dom h ) by A2, A3, FINSEQ_3:27;
i < i + 1 by NAT_1:16;
hence h . i < h . (i + 1) by A1, A4, VALUED_0:def 13; :: thesis: verum

end;

assume A5: for i being Nat st 1 <= i & i < len h holds
h . i < h . (i + 1) ; :: thesis: h is increasing

now

let n, m be ext-real number ; :: thesis: ( n in dom h & m in dom h & n < m implies h . n < h . m )
assume C1: n in dom h ; :: thesis: ( m in dom h & n < m implies h . n < h . m )
then A6: ( 1 <= n & n <= len h ) by FINSEQ_3:27;
assume C2: m in dom h ; :: thesis: ( n < m implies h . n < h . m )
then A7: ( 1 <= m & m <= len h ) by FINSEQ_3:27;
reconsider m1 = m, n1 = n as Element of NAT by C1, C2;
assume n < m ; :: thesis: h . n < h . m
then consider k being Nat such that
A8: m1 = (n1 + 1) + k by Lm1;
defpred S₁[ Nat] means ( n1 + $1 < len h implies h . n < h . ((n1 + 1) + $1) );
m1 - 1 < (len h) - 0 by A7, XREAL_1:17;
then A9: n1 + k < len h by A8;
A10: S₁[ 0 ] by A6, A5;

A11: now

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume A12: S₁[a] ; :: thesis: S₁[a + 1]
thus S₁[a + 1] :: thesis: verum

proof

assume A13: n1 + (a + 1) < len h ; :: thesis: h . n < h . ((n1 + 1) + (a + 1))
1 <= 1 + (n1 + a) by NAT_1:11;
then A14: h . ((n1 + 1) + a) < h . (((n1 + 1) + a) + 1) by A5, A13;
(n1 + a) + 0 < (n1 + a) + 1 by XREAL_1:8;
hence h . n < h . ((n1 + 1) + (a + 1)) by A12, A13, A14, XXREAL_0:2; :: thesis: verum

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A11);
hence h . n < h . m by A8, A9; :: thesis: verum

end;

hence h is increasing by VALUED_0:def 13; :: thesis: verum