let f be Form of V,V; :: thesis: ( f is hermitan implies f is diagRvalued )

assume A1: f is hermitan ; :: thesis: f is diagRvalued

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

f . (v,v) = (f . (v,v)) *' by A1;

hence Im (f . (v,v)) = 0 by Th1; :: thesis: verum

assume A1: f is hermitan ; :: thesis: f is diagRvalued

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

f . (v,v) = (f . (v,v)) *' by A1;

hence Im (f . (v,v)) = 0 by Th1; :: thesis: verum