let v be Vector of V; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (- f) . (a * v) = (a *' ) * ((- f) . v)
let a be Scalar of ; :: thesis: (- f) . (a * v) = (a *' ) * ((- f) . v)
thus (- f) . (a * v) = - (f . (a * v)) by HAHNBAN1:def 7
.= - ((a *' ) * (f . v)) by Def1
.= (a *' ) * (- (f . v)) by VECTSP_1:41
.= (a *' ) * ((- f) . v) by HAHNBAN1:def 7 ; :: thesis: verum