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