let V be VectSp of F_Complex ; :: thesis: for f being diagReR+0valued hermitan-Form of V holds diagker f = leftker f
let f be diagReR+0valued hermitan-Form of V; :: thesis: diagker f = leftker f
thus diagker f c= leftker f :: according to XBOOLE_0:def 10 :: thesis: leftker f c= diagker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in diagker f or x in leftker f )
assume x in diagker f ; :: thesis: x in leftker f
then consider a being Vector of V such that
A1: a = x and
A2: f . (a,a) = 0. F_Complex ;

now :: thesis: for w being Vector of V holds f . (a,w) = 0. F_Complex

let w be Vector of V; :: thesis: f . (a,w) = 0. F_Complex
|.(f . (a,w)).| ^2 <= 0 * |.(f . (w,w)).| by A2, Th46, COMPLFLD:57;
then |.(f . (a,w)).| = 0 by XREAL_1:63;
hence f . (a,w) = 0. F_Complex by COMPLFLD:58; :: thesis: verum

end;

hence x in leftker f by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in diagker f )
assume x in leftker f ; :: thesis: x in diagker f
then consider a being Vector of V such that
A3: a = x and
A4: for w being Vector of V holds f . (a,w) = 0. F_Complex ;
f . (a,a) = 0. F_Complex by A4;
hence x in diagker f by A3; :: thesis: verum