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 A2: v = 0. V ; :: thesis: 0 <= Re (f . (v,v))

A3: [**(Re (0. F_Complex)),(Im (0. F_Complex))**] = [**0,0**] by COMPLEX1:13, COMPLFLD:7;
f . (v,v) = 0. F_Complex by A1, A2, BILINEAR:29;
hence 0 <= Re (f . (v,v)) by A3, COMPLEX1:77; :: thesis: verum

end;

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

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

end;

end;