let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L
let L be Z_Linear_Combination of V; :: thesis: - (vector ((LC_Z_Module V),L)) = - L
thus - (vector ((LC_Z_Module V),L)) = (- 1) * (vector ((LC_Z_Module V),L)) by ZMODUL01:2
.= - L by Th48 ; :: thesis: verum