let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds - (vector (LC_RLSpace V),L) = - L
let L be Linear_Combination of V; :: thesis: - (vector (LC_RLSpace V),L) = - L
thus - (vector (LC_RLSpace V),L) = (- 1) * (vector (LC_RLSpace V),L) by RLVECT_1:29
.= - L by Th97 ; :: thesis: verum