theorem Th42: :: ZMODUL02:42
for V being Z_Module
for L being Linear_Combination of V holds L - L = ZeroLC V by VECTSP_6:43;