let v be Vector of V; :: according to HERMITAN:def 7 :: thesis: 0 <= Re ((NulForm (V,V)) . (v,v))
Re (0. F_Complex) = In (0,REAL) by COMPLEX1:def 1, COMPLFLD:7;
hence 0 <= Re ((NulForm (V,V)) . (v,v)) by FUNCOP_1:70; :: thesis: verum