theorem Th25: :: ZMODUL03:25

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for X being non empty Subset of (Z_MQ_VectSp (V,p)) st X = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } holds
ex F being Function of X, the carrier of V st
( ( 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 )