let v be FinSequence of REAL ; :: thesis: ( v <> {} implies Incr v <> {} )
assume A1: v <> {} ; :: thesis: Incr v <> {}
assume Incr v = {} ; :: thesis: contradiction
then ( len (Incr v) = 0 & len (Incr v) = card (rng v) & rng v is finite ) by Def2;
then ( rng v = {} & rng v <> {} ) by A1, RELAT_1:64;
hence contradiction ; :: thesis: verum