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

proof

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

now

let w be Vector of V; :: thesis: f . w,a = 0. F_Complex
( |.(f . w,a).| ^2 <= |.(f . w,w).| * 0 & 0 <= |.(f . w,a).| ^2 ) by A1, Th49, COMPLFLD:93, XREAL_1:65;
then |.(f . w,a).| ^2 = 0 ;
then |.(f . w,a).| = 0 ;
hence f . w,a = 0. F_Complex by COMPLFLD:94; :: thesis: verum

end;

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

end;

thus rightker f c= diagker f by BILINEAR:42; :: thesis: verum