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

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