let v, w be Vector of V; :: according to BILINEAR:def 25 :: thesis: (NulForm (V,V)) . (v,w) = (NulForm (V,V)) . (w,v)

thus (NulForm (V,V)) . (v,w) = 0. K by FUNCOP_1:70

.= (NulForm (V,V)) . (w,v) by FUNCOP_1:70 ; :: thesis: verum

thus (NulForm (V,V)) . (v,w) = 0. K by FUNCOP_1:70

.= (NulForm (V,V)) . (w,v) by FUNCOP_1:70 ; :: thesis: verum