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)

per cases ( v = 0. V or v <> 0. V ) ;

suppose v = 0. V ; :: thesis: 0 <= Re (f . v,v)

then A2: f . v,v = 0. F_Complex by A1, BILINEAR:30;
[**(Re (0. F_Complex )),(Im (0. F_Complex ))**] = [**0 ,0 **] by COMPLEX1:29, COMPLFLD:9;
hence 0 <= Re (f . v,v) by A2, COMPLEX1:163; :: thesis: verum

end;

suppose v <> 0. V ; :: thesis: 0 <= Re (f . v,v)

hence 0 <= Re (f . v,v) by A1, Def13; :: thesis: verum

end;

end;