theorem Th24: :: ZMODUL03:24

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for lq being Linear_Combination of Z_MQ_VectSp (V,p) ex l being Linear_Combination of I st
for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v))