let f be Form of V,V; :: thesis: ( f is positivediagvalued & f is additiveFAF implies f is diagReR+0valued )

assume A1: ( f is positivediagvalued & f is additiveFAF ) ; :: thesis: f is diagReR+0valued

let v be Vector of V; :: according to HERMITAN:def 7 :: thesis: 0 <= Re (f . (v,v))

assume A1: ( f is positivediagvalued & f is additiveFAF ) ; :: thesis: f is diagReR+0valued

let v be Vector of V; :: according to HERMITAN:def 7 :: thesis: 0 <= Re (f . (v,v))