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
( i < j or i = j ) by A2, XXREAL_0:1;
hence h . i <= h . j by A1, A3, A4, Th5; :: thesis: verum