let V be non empty VectSpStr of 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 set ; :: 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 & f . v = 0. F_Complex ) ;
(f *' ) . v = 0. F_Complex by A1, Th25;
hence x in ker (f *' ) by A1; :: thesis: verum

end;

let x be set ; :: 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
A2: ( x = v & (f *' ) . v = 0. F_Complex ) ;
f . v = 0. F_Complex by A2, Th25;
hence x in ker f by A2; :: thesis: verum