let V, W be non empty VectSpStr of 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 set ; :: 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

let w be Vector of W; :: thesis: (f *' ) . v,w = 0. F_Complex
(f . v,w) *' = 0. F_Complex by A2, COMPLFLD:83;
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 set ; :: 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

let w be Vector of W; :: thesis: f . v,w = 0. F_Complex
((f *' ) . v,w) *' = 0. F_Complex by A4, COMPLFLD:83;
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 set ; :: 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

let v be Vector of V; :: thesis: (f *' ) . v,w = 0. F_Complex
(f . v,w) *' = 0. F_Complex by A6, COMPLFLD:83;
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 set ; :: 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

let v be Vector of V; :: thesis: f . v,w = 0. F_Complex
((f *' ) . v,w) *' = 0. F_Complex by A8, COMPLFLD:83;
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