let p be prime Element of INT.Ring; 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; 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; 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 A4:
not
I is
empty
;
card { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } = card Ithen 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;
verum end; end;