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 Th28; :: thesis: verum