set K = F_Complex ;
let V be non empty VectSpStr of F_Complex ; :: thesis: for f being Form of V,V holds diagker f = diagker (f *' )
let f be Form of V,V; :: thesis: diagker f = diagker (f *' )
thus diagker f c= diagker (f *' ) :: according to XBOOLE_0:def 10 :: thesis: diagker (f *' ) c= diagker f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in diagker f or x in diagker (f *' ) )
assume x in diagker f ; :: thesis: x in diagker (f *' )
then consider v being Vector of V such that
A1: ( x = v & f . v,v = 0. F_Complex ) ;
(f *' ) . v,v = 0. F_Complex by A1, Def8, COMPLFLD:83;
hence x in diagker (f *' ) by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in diagker (f *' ) or x in diagker f )
assume x in diagker (f *' ) ; :: thesis: x in diagker f
then consider v being Vector of V such that
A2: ( x = v & (f *' ) . v,v = 0. F_Complex ) ;
((f . v,v) *' ) *' = 0. F_Complex by A2, Def8, COMPLFLD:83;
hence x in diagker f by A2; :: thesis: verum