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

proof

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

proof

A6: k < k + 1 by XREAL_1:29;
assume A7: k + 1 <= len h ; :: thesis: k + 1 <= h . (k + 1)
then A8: k < len h by A6, XXREAL_0:2;

per cases ( k = 0 or k > 0 ) ;

suppose k = 0 ; :: thesis: k + 1 <= h . (k + 1)

hence k + 1 <= h . (k + 1) by A3; :: thesis: verum

end;

suppose k > 0 ; :: thesis: k + 1 <= h . (k + 1)

then 0 + 1 <= k by NAT_1:13;
then h . k < h . (k + 1) by A1, A8;
then k < h . (k + 1) by A5, A7, A6, XXREAL_0:2;
hence k + 1 <= h . (k + 1) by NAT_1:13; :: thesis: verum

end;

end;

end;

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

end;

A9: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A4);
hence i <= h . i by A2; :: thesis: verum