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

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

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 )
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;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

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