let v be FinSequence of REAL ; :: thesis: ( v is increasing implies for n, m being Nat st n in dom v & m in dom v & n <= m holds
v . n <= v . m )
assume A1: v is increasing ; :: thesis: for n, m being Nat st n in dom v & m in dom v & n <= m holds
v . n <= v . m
let n, m be Nat; :: thesis: ( n in dom v & m in dom v & n <= m implies v . n <= v . m )
assume that
A2: ( n in dom v & m in dom v ) and
A3: n <= m ; :: thesis: v . n <= v . m

now :: thesis: v . n <= v . m

per cases ( n = m or n <> m ) ;

suppose n = m ; :: thesis: v . n <= v . m

hence v . n <= v . m ; :: thesis: verum

end;

suppose n <> m ; :: thesis: v . n <= v . m

then n < m by A3, XXREAL_0:1;
hence v . n <= v . m by A1, A2, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence v . n <= v . m ; :: thesis: verum