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

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