let v be FinSequence of REAL ; :: thesis: ( card (rng v) = 0 implies ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) )
assume card (rng v) = 0 ; :: thesis: ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
then A1: rng v = {} ;
then A2: v = {} by RELAT_1:64;
take v1 = v; :: thesis: ( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing )
thus rng v1 = rng v ; :: thesis: ( len v1 = card (rng v) & v1 is increasing )
thus len v1 = card (rng v) by A1, RELAT_1:64; :: thesis: v1 is increasing
for n, m being Element of NAT st n in dom v1 & m in dom v1 & n < m holds
v1 . n < v1 . m by A2, RELAT_1:60;
hence v1 is increasing by SEQM_3:def 1; :: thesis: verum