set f = NulFrForm (V,V);

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

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

proof

hence
NulFrForm (V,V) is symmetric
; :: thesis: verum
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;thus (NulFrForm (V,V)) . (v,w) = 0. F_Real by FUNCOP_1:70

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