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)
A4: 1 <= i + 1 by NAT_1:12;
i + 1 <= len h by A3, NAT_1:13;
then A5: i + 1 in dom h by A4, FINSEQ_3:25;
A6: i < i + 1 by NAT_1:16;
i in dom h by A2, A3, FINSEQ_3:25;
hence h . i < h . (i + 1) by A1, A5, A6, VALUED_0:def 13; :: thesis: verum

end;

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

now :: thesis: for n, m being ExtReal st n in dom h & m in dom h & n < m holds
h . n < h . m

let n, m be ExtReal; :: thesis: ( n in dom h & m in dom h & n < m implies h . n < h . m )
assume A8: n in dom h ; :: thesis: ( m in dom h & n < m implies h . n < h . m )
assume A9: m in dom h ; :: thesis: ( n < m implies h . n < h . m )
then reconsider m1 = m, n1 = n as Element of NAT by A8;
defpred S₁[ Nat] means ( n1 + $1 < len h implies h . n < h . ((n1 + 1) + $1) );

A10: now :: thesis: for a being Nat st S₁[a] holds
S₁[a + 1]

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

proof

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

end;

end;

1 <= n by A8, FINSEQ_3:25;
then A14: S₁[ 0 ] by A7;
A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A10);
assume n < m ; :: thesis: h . n < h . m
then consider k being Nat such that
A16: m1 = (n1 + 1) + k by Lm2;
m <= len h by A9, FINSEQ_3:25;
then m1 - 1 < (len h) - 0 by XREAL_1:15;
then n1 + k < len h by A16;
hence h . n < h . m by A16, A15; :: thesis: verum

end;

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