theorem Th22: :: ZMODUL03:22

for p being prime Element of INT.Ring
for V being Z_Module
for ZQ being VectSp of GF p
for vq being Vector of ZQ st ZQ = Z_MQ_VectSp (V,p) holds
ex v being Vector of V st vq = ZMtoMQV (V,p,v)