let v be Vector of V; :: according to HERMITAN:def 1 :: thesis: for a being Scalar of holds (a * f) . (a * v) = (a *') * ((a * f) . v)

let b be Scalar of ; :: thesis: (a * f) . (b * v) = (b *') * ((a * f) . v)

thus (a * f) . (b * v) = a * (f . (b * v)) by HAHNBAN1:def 6

.= a * ((b *') * (f . v)) by Def1

.= (b *') * (a * (f . v))

.= (b *') * ((a * f) . v) by HAHNBAN1:def 6 ; :: thesis: verum

let b be Scalar of ; :: thesis: (a * f) . (b * v) = (b *') * ((a * f) . v)

thus (a * f) . (b * v) = a * (f . (b * v)) by HAHNBAN1:def 6

.= a * ((b *') * (f . v)) by Def1

.= (b *') * (a * (f . v))

.= (b *') * ((a * f) . v) by HAHNBAN1:def 6 ; :: thesis: verum