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:4
.= - L by Th39 ; :: thesis: verum