consider v1 being FinSequence of REAL such that
A1: ( rng v1 = rng v & len v1 = card (rng v) ) and
A2: v1 is increasing by Lm12;
reconsider v1 = v1 as increasing FinSequence of REAL by A2;
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