let v, w be Vector of V; :: according to BILINEAR:def 25 :: thesis: (a * f) . (v,w) = (a * f) . (w,v)
thus (a * f) . (v,w) = a * (f . (v,w)) by Def3
.= a * (f . (w,v)) by Def25
.= (a * f) . (w,v) by Def3 ; :: thesis: verum