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);

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 )
;

end;

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 } = {}

end;proof

hence
card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card I
by A1; :: thesis: verum
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;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

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

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;

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))

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;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;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

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