consider v1 being FinSequence of REAL such that
A1: ( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm6;
reconsider v1 = v1 as increasing FinSequence of REAL by A1;
take v1 ; :: thesis: ( rng v1 = rng v & len v1 = card (rng v) )
thus ( rng v1 = rng v & len v1 = card (rng v) ) by A1; :: thesis: verum