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