theorem Th31: :: ZMODUL03:31

for p being prime Element of INT.Ring
for V being free Z_Module
for I being Basis of V
for l being Linear_Combination of I
for IQ being Subset of (Z_MQ_VectSp (V,p))
for lq being Linear_Combination of IQ st IQ = { (ZMtoMQV (V,p,u)) where u is Vector of V : u in I } & ( for v being Vector of V st v in I holds
l . v = lq . (ZMtoMQV (V,p,v)) ) holds
Sum lq = ZMtoMQV (V,p,(Sum l))