let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V holds L - L = Z_ZeroLC V
let L be Z_Linear_Combination of V; :: thesis: L - L = Z_ZeroLC V
let v be VECTOR of V; :: according to ZMODUL02:def 24 :: thesis: (L - L) . v = (Z_ZeroLC V) . v
thus (L - L) . v = (L . v) - (L . v) by Th39
.= (Z_ZeroLC V) . v by Th9 ; :: thesis: verum