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