let V be non empty ModuleStr over 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 *')
set K = F_Complex ;
thus diagker f c= diagker (f *') :: according to XBOOLE_0:def 10 :: thesis: diagker (f *') c= diagker f
proof
let x be object ; :: 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 and
A2: f . (v,v) = 0. F_Complex ;
(f *') . (v,v) = 0. F_Complex by A2, Def8, COMPLFLD:47;
hence x in diagker (f *') by A1; :: thesis: verum
end;
let x be object ; :: 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
A3: x = v and
A4: (f *') . (v,v) = 0. F_Complex ;
((f . (v,v)) *') *' = 0. F_Complex by A4, Def8, COMPLFLD:47;
hence x in diagker f by A3; :: thesis: verum