let V be non empty VectSpStr of 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:83; :: 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:83;
hence f . v = 0. F_Complex ; :: thesis: verum