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 A2: ( i <= j & 1 <= i & j <= len h ) ; :: thesis: h . i <= h . j
then ( i < j or i = j ) by XXREAL_0:1;
hence h . i <= h . j by Th9, A2, A1; :: thesis: verum