theorem Th57: :: RLVECT_2:57

for V being RealLinearSpace
for L being Linear_Combination of V holds L - L = ZeroLC V