theorem :: ZMODUL02:39

for V being Z_Module
for v being VECTOR of V
for L1, L2 being Linear_Combination of V holds (L1 - L2) . v = (L1 . v) - (L2 . v) by VECTSP_6:40;