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