theorem :: ZMODUL02:10

for V being Z_Module
for A, B being Subset of V
for l being Linear_Combination of A st A c= B holds
l is Linear_Combination of B by VECTSP_6:4;