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