take v = <*0 *>; :: thesis: ( not v is empty & v is increasing )
thus not v is empty ; :: thesis: v is increasing
let n be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b₁ being Element of NAT holds
( not n in proj1 v or not b₁ in proj1 v or b₁ <= n or not v . b₁ <= v . n )
let m be Element of NAT ; :: thesis: ( not n in proj1 v or not m in proj1 v or m <= n or not v . m <= v . n )
assume that
A1: n in dom v and
A2: m in dom v ; :: thesis: ( m <= n or not v . m <= v . n )
A3: dom <*0 *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then n = 1 by A1, TARSKI:def 1;
hence ( m <= n or not v . m <= v . n ) by A3, A2, TARSKI:def 1; :: thesis: verum