let R be Ring; :: thesis: for V being LeftMod of R

for L being Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L

let V be LeftMod of R; :: thesis: for L being Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L

let L be Linear_Combination of V; :: thesis: - (vector ((LC_Z_Module V),L)) = - L

thus - (vector ((LC_Z_Module V),L)) = (- (1. R)) * (vector ((LC_Z_Module V),L)) by ZMODUL01:2

.= - L by Th48 ; :: thesis: verum

for L being Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L

let V be LeftMod of R; :: thesis: for L being Linear_Combination of V holds - (vector ((LC_Z_Module V),L)) = - L

let L be Linear_Combination of V; :: thesis: - (vector ((LC_Z_Module V),L)) = - L

thus - (vector ((LC_Z_Module V),L)) = (- (1. R)) * (vector ((LC_Z_Module V),L)) by ZMODUL01:2

.= - L by Th48 ; :: thesis: verum