take v = <*(In (0,REAL))*>; :: thesis: ( not v is empty & v is increasing )
thus not v is empty ; :: thesis: v is increasing
let n be Nat; :: according to SEQM_3:def 1 :: thesis: for n being Nat st n in dom v & n in dom v & n < n holds
v . n < v . n
let m be Nat; :: thesis: ( n in dom v & m in dom v & n < m implies v . n < v . m )
assume that
A1: n in dom v and
A2: m in dom v ; :: thesis: ( not n < m or v . n < v . m )
A3: dom <*0*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by A1, TARSKI:def 1;
hence ( not n < m or v . n < v . m ) by A3, A2, TARSKI:def 1; :: thesis: verum