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