the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def 11;
hence QFunctional (f,(Ker (f *'))) is antilinear-Functional of (VectQuot (V,(Ker (f *')))) by Th25; :: thesis: verum