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:16

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

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:16

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