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

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