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 = {} ;
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:41; :: thesis: v1 is increasing
for n, m being Nat st n in dom v1 & m in dom v1 & n < m holds
v1 . n < v1 . m by A1, RELAT_1:38, RELAT_1:41;
hence v1 is increasing by SEQM_3:def 1; :: thesis: verum