let V be non empty ModuleStr over F_Complex ; :: thesis: for f being Functional of V holds ker f = ker (f *')
let f be Functional of V; :: thesis: ker f = ker (f *')
thus ker f c= ker (f *') :: according to XBOOLE_0:def 10 :: thesis: ker (f *') c= ker f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker f or x in ker (f *') )
assume x in ker f ; :: thesis: x in ker (f *')
then consider v being Vector of V such that
A1: x = v and
A2: f . v = 0. F_Complex ;
(f *') . v = 0. F_Complex by A2, Th22;
hence x in ker (f *') by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker (f *') or x in ker f )
assume x in ker (f *') ; :: thesis: x in ker f
then consider v being Vector of V such that
A3: x = v and
A4: (f *') . v = 0. F_Complex ;
f . v = 0. F_Complex by A4, Th22;
hence x in ker f by A3; :: thesis: verum