:: deftheorem Def21 defines Incr SEQ_4:def 21 :
for v being FinSequence of REAL
for b₂ being increasing FinSequence of REAL holds
( b₂ = Incr v iff ( rng b₂ = rng v & len b₂ = card (rng v) ) );