let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ModuleStr over 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 Th23;
hence ker f is linearly-closed by VECTSP10:33; :: thesis: verum