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 4
.= - ((a *') * (f . v)) by Def1
.= (a *') * (- (f . v)) by VECTSP_1:9
.= (a *') * ((- f) . v) by HAHNBAN1:def 4 ; :: thesis: verum