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 *') )

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 ;

( 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

thus
leftker (f *') c= leftker f
:: thesis: rightker f = rightker (f *')
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 ;

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

hence
x in leftker (f *')
by A1; :: thesis: verumlet 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;(f . (v,w)) *' = 0. F_Complex by A2, COMPLFLD:47;

hence (f *') . (v,w) = 0. F_Complex by Def8; :: thesis: verum

proof

thus
rightker f c= rightker (f *')
:: according to XBOOLE_0:def 10 :: thesis: rightker (f *') c= rightker f
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 ;

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

hence
x in leftker f
by A3; :: thesis: verumlet 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;((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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rightker (f *') or x in rightker f )
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 ;

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

hence
x in rightker (f *')
by A5; :: thesis: verumlet 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;(f . (v,w)) *' = 0. F_Complex by A6, COMPLFLD:47;

hence (f *') . (v,w) = 0. F_Complex by Def8; :: thesis: verum

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

hence
x in rightker f
by A7; :: thesis: verumlet 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;((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