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