let h be real-valued FinSequence; :: thesis: ( h is increasing implies for i, j being Nat st i < j & 1 <= i & j <= len h holds
h . i < h . j )
assume A1: h is increasing ; :: thesis: for i, j being Nat st i < j & 1 <= i & j <= len h holds
h . i < h . j
let i, j be Nat; :: thesis: ( i < j & 1 <= i & j <= len h implies h . i < h . j )
assume that
A2: i < j and
A3: 1 <= i and
A4: j <= len h ; :: thesis: h . i < h . j
defpred S₁[ Nat] means ( (i + 1) + $1 <= len h implies h . i < h . ((i + 1) + $1) );
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
( (i + 1) + (k + 1) <= len h implies h . i < h . ((i + 1) + (k + 1)) )

proof

A7: i + 1 <= (i + 1) + k by NAT_1:11;
i < i + 1 by XREAL_1:31;
then i < (i + 1) + k by A7, XXREAL_0:2;
then A8: 1 < (i + 1) + k by A3, XXREAL_0:2;
k < k + 1 by XREAL_1:31;
then A9: (i + 1) + k < (i + 1) + (k + 1) by XREAL_1:8;
assume A10: (i + 1) + (k + 1) <= len h ; :: thesis: h . i < h . ((i + 1) + (k + 1))
then (i + 1) + k < len h by A9, XXREAL_0:2;
then h . ((i + 1) + k) < h . (((i + 1) + k) + 1) by A1, A8, Def1;
hence h . i < h . ((i + 1) + (k + 1)) by A6, A10, A9, XXREAL_0:2; :: thesis: verum

end;

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

end;

i < len h by A2, A4, XXREAL_0:2;
then A11: S₁[ 0 ] by A1, A3, Def1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A5);
then A12: ( (i + 1) + (j -' (i + 1)) <= len h implies h . i < h . ((i + 1) + (j -' (i + 1))) ) ;
i + 1 <= j by A2, NAT_1:13;
then j -' (i + 1) = j - (i + 1) by XREAL_1:235;
hence h . i < h . j by A4, A12; :: thesis: verum