let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr of F_Complex ; :: thesis: for f being antilinear-Functional of V holds ker f is linearly-closed
let f be antilinear-Functional of V; :: thesis: ker f is linearly-closed
ker f = ker (f *' ) by Th26;
hence ker f is linearly-closed by VECTSP10:34; :: thesis: verum