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 set ; :: 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 & f . a,a = 0. F_Complex ) ;

now

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

end;

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

end;

let x be set ; :: 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
A2: ( a = x & ( for w being Vector of V holds f . a,w = 0. F_Complex ) ) ;
f . a,a = 0. F_Complex by A2;
hence x in diagker f by A2; :: thesis: verum