theorem ThQuotBasis5:
for
p being
prime Element of
INT.Ring for
V being
free Z_Module for
I being
Subset of
V for
IQ being
Subset of
(Z_MQ_VectSp (V,p)) st
Lin I = ModuleStr(# the
carrier of
V, the
addF of
V, the
ZeroF of
V, the
lmult of
V #) &
IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
Lin IQ = ModuleStr(# the
carrier of
(Z_MQ_VectSp (V,p)), the
addF of
(Z_MQ_VectSp (V,p)), the
ZeroF of
(Z_MQ_VectSp (V,p)), the
lmult of
(Z_MQ_VectSp (V,p)) #)