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