the carrier of (Ker f) = ker f by Def11;
hence QFunctional (f,(Ker f)) is linear-Functional of (VectQuot (V,(Ker f))) by Th34; :: thesis: verum