take v = <*0 *>; :: thesis: ( not v is empty & v is increasing )
A1: dom <*0 *> = {1} by FINSEQ_1:4, FINSEQ_1:55;
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 dom v or not b₁ in dom v or b₁ <= n or not v . b₁ <= v . n )
let m be Element of NAT ; :: thesis: ( not n in dom v or not m in dom v or m <= n or not v . m <= v . n )
assume ( n in dom v & m in dom v ) ; :: thesis: ( m <= n or not v . m <= v . n )
then ( n = 1 & m = 1 ) by A1, TARSKI:def 1;
hence ( m <= n or not v . m <= v . n ) ; :: thesis: verum