let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V holds - (- L) = L
let L be Linear_Combination of V; :: thesis: - (- L) = L
let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: (- (- L)) . v = L . v
thus (- (- L)) . v = (((- 1) * (- 1)) * L) . v by Th47
.= 1 * (L . v) by Def11
.= L . v ; :: thesis: verum