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 object ; :: 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 and
A2: f . (a,a) = 0. F_Complex ;
now :: thesis: for w being Vector of V holds f . (w,a) = 0. F_Complex
let w be Vector of V; :: thesis: f . (w,a) = 0. F_Complex
|.(f . (w,a)).| ^2 <= |.(f . (w,w)).| * 0 by A2, Th46, COMPLFLD:57;
then |.(f . (w,a)).| = 0 by XREAL_1:63;
hence f . (w,a) = 0. F_Complex by COMPLFLD:58; :: thesis: verum
end;
hence x in rightker f by A1; :: thesis: verum
end;
thus rightker f c= diagker f by BILINEAR:41; :: thesis: verum