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

per cases ( I is empty or not I is empty ) ;

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

{ (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: contradiction
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: verum

end;

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

end;

suppose A4: not I is empty ; :: thesis: card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I

now :: thesis: for x being object st x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
x in the carrier of (Z_MQ_VectSp (V,p))

let x be object ; :: thesis: ( x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } implies x in the carrier of (Z_MQ_VectSp (V,p)) )
assume x in { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } ; :: thesis: x in the carrier of (Z_MQ_VectSp (V,p))
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: verum

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: verum

end;

end;