let p be prime Element of INT.Ring; :: thesis:
let V be free Z_Module; :: thesis:
let I be Basis of V; :: thesis:
set X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ;
set ZQ = Z_MQ_VectSp (V,p);

per cases ;

suppose A1: I is empty ; :: thesis:

{ (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = {}

proof

assume { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } <> {} ; :: thesis:
then consider v0 being object such that
A2: v0 in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } by XBOOLE_0:def 1;
consider u being Vector of V such that
A3: ( v0 = ZMtoMQV (V,p,u) & u in I ) by A2;
thus contradiction by A3, A1; :: thesis:

end;

hence card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I by A1; :: thesis:

end;

suppose A4: not I is empty ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
assume x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis:
then consider v being Vector of V such that
A5: ( x = ZMtoMQV (V,p,v) & v in I ) ;
thus x in the carrier of (Z_MQ_VectSp (V,p)) by A5; :: thesis:

end;

then reconsider X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } as Subset of (Z_MQ_VectSp (V,p)) by TARSKI:def 3;
consider v0 being object such that
A6: v0 in I by A4, XBOOLE_0:def 1;
reconsider v0 = v0 as Vector of V by A6;
ZMtoMQV (V,p,v0) in X by A6;
then reconsider X = X as non empty Subset of (Z_MQ_VectSp (V,p)) ;
consider F being Function of X, the carrier of V such that
A7: ( ( for u being Vector of V st u in I holds
F . (ZMtoMQV (V,p,u)) = u ) & F is one-to-one & dom F = X & rng F = I ) by Th25;
thus card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I by A7, CARD_1:5, WELLORD2:def 4; :: thesis:

end;

end;