let V be non empty CLSStruct ; :: thesis: for L being C_Linear_Combination of V holds - (vector ((LC_CLSpace V),L)) = - L
let L be C_Linear_Combination of V; :: thesis: - (vector ((LC_CLSpace V),L)) = - L
thus - (vector ((LC_CLSpace V),L)) = (- 1r) * (vector ((LC_CLSpace V),L)) by CLVECT_1:3
.= - L by Th39 ; :: thesis: verum