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