theorem Th23: :: ZMODUL03:23

for p being prime Element of INT.Ring
for V being Z_Module
for I being Subset 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
ex w being Vector of V st
( w in I & w in ZMtoMQV (V,p,v) & l . w = lq . (ZMtoMQV (V,p,v)) )