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

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

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

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