let V, W be non empty ModuleStr over F_Complex ; :: thesis: for f being Form of V,W holds
( leftker f = leftker (f *') & rightker f = rightker (f *') )
let f be Form of V,W; :: thesis: ( leftker f = leftker (f *') & rightker f = rightker (f *') )
set K = F_Complex ;
thus leftker f c= leftker (f *') :: according to XBOOLE_0:def 10 :: thesis: ( leftker (f *') c= leftker f & rightker f = rightker (f *') )

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker f or x in leftker (f *') )
assume x in leftker f ; :: thesis: x in leftker (f *')
then consider v being Vector of V such that
A1: x = v and
A2: for w being Vector of W holds f . (v,w) = 0. F_Complex ;

now :: thesis: for w being Vector of W holds (f *') . (v,w) = 0. F_Complex

let w be Vector of W; :: thesis: (f *') . (v,w) = 0. F_Complex
(f . (v,w)) *' = 0. F_Complex by A2, COMPLFLD:47;
hence (f *') . (v,w) = 0. F_Complex by Def8; :: thesis: verum

end;

hence x in leftker (f *') by A1; :: thesis: verum

end;

thus leftker (f *') c= leftker f :: thesis: rightker f = rightker (f *')

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in leftker (f *') or x in leftker f )
assume x in leftker (f *') ; :: thesis: x in leftker f
then consider v being Vector of V such that
A3: x = v and
A4: for w being Vector of W holds (f *') . (v,w) = 0. F_Complex ;

now :: thesis: for w being Vector of W holds f . (v,w) = 0. F_Complex

let w be Vector of W; :: thesis: f . (v,w) = 0. F_Complex
((f *') . (v,w)) *' = 0. F_Complex by A4, COMPLFLD:47;
then ((f . (v,w)) *') *' = 0. F_Complex by Def8;
hence f . (v,w) = 0. F_Complex ; :: thesis: verum

end;

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

end;

thus rightker f c= rightker (f *') :: according to XBOOLE_0:def 10 :: thesis: rightker (f *') c= rightker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker f or x in rightker (f *') )
assume x in rightker f ; :: thesis: x in rightker (f *')
then consider w being Vector of W such that
A5: x = w and
A6: for v being Vector of V holds f . (v,w) = 0. F_Complex ;

now :: thesis: for v being Vector of V holds (f *') . (v,w) = 0. F_Complex

let v be Vector of V; :: thesis: (f *') . (v,w) = 0. F_Complex
(f . (v,w)) *' = 0. F_Complex by A6, COMPLFLD:47;
hence (f *') . (v,w) = 0. F_Complex by Def8; :: thesis: verum

end;

hence x in rightker (f *') by A5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (f *') or x in rightker f )
assume x in rightker (f *') ; :: thesis: x in rightker f
then consider w being Vector of W such that
A7: x = w and
A8: for v being Vector of V holds (f *') . (v,w) = 0. F_Complex ;

now :: thesis: for v being Vector of V holds f . (v,w) = 0. F_Complex

let v be Vector of V; :: thesis: f . (v,w) = 0. F_Complex
((f *') . (v,w)) *' = 0. F_Complex by A8, COMPLFLD:47;
then ((f . (v,w)) *') *' = 0. F_Complex by Def8;
hence f . (v,w) = 0. F_Complex ; :: thesis: verum

end;

hence x in rightker f by A7; :: thesis: verum