let V be non empty ModuleStr over F_Complex ; :: thesis: for f being Functional of V

for v being Vector of V holds

( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

let f be Functional of V; :: thesis: for v being Vector of V holds

( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

let v be Vector of V; :: thesis: ( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

thus ( f . v = 0. F_Complex implies (f *') . v = 0. F_Complex ) by Def2, COMPLFLD:47; :: thesis: ( (f *') . v = 0. F_Complex implies f . v = 0. F_Complex )

assume (f *') . v = 0. F_Complex ; :: thesis: f . v = 0. F_Complex

then ((f . v) *') *' = 0. F_Complex by Def2, COMPLFLD:47;

hence f . v = 0. F_Complex ; :: thesis: verum

for v being Vector of V holds

( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

let f be Functional of V; :: thesis: for v being Vector of V holds

( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

let v be Vector of V; :: thesis: ( f . v = 0. F_Complex iff (f *') . v = 0. F_Complex )

thus ( f . v = 0. F_Complex implies (f *') . v = 0. F_Complex ) by Def2, COMPLFLD:47; :: thesis: ( (f *') . v = 0. F_Complex implies f . v = 0. F_Complex )

assume (f *') . v = 0. F_Complex ; :: thesis: f . v = 0. F_Complex

then ((f . v) *') *' = 0. F_Complex by Def2, COMPLFLD:47;

hence f . v = 0. F_Complex ; :: thesis: verum