theorem Th13: :: ZMODUL03:13

for V being Z_Module
for W being Submodule of V
for L being Linear_Combination of V st Carrier L c= the carrier of W holds
ex K being Linear_Combination of W st
( Carrier K = Carrier L & Sum K = Sum L )