set f = NulFrForm (V,V);
for v, w being Vector of V holds (NulFrForm (V,V)) . (v,w) = (NulFrForm (V,V)) . (w,v)

proof

let v, w be Vector of V; :: thesis: (NulFrForm (V,V)) . (v,w) = (NulFrForm (V,V)) . (w,v)
thus (NulFrForm (V,V)) . (v,w) = 0. F_Real by FUNCOP_1:70
.= (NulFrForm (V,V)) . (w,v) by FUNCOP_1:70 ; :: thesis: verum

end;

hence NulFrForm (V,V) is symmetric ; :: thesis: verum