set qf = CQFunctional f;
set W = Ker f;
set qV = VectQuot (V,(Ker f));
A1: the carrier of (Ker f) = ker f by Def11;
A2: the carrier of (VectQuot (V,(Ker f))) = CosetSet (V,(Ker f)) by Def6;
thus ker (CQFunctional f) c= {(0. (VectQuot (V,(Ker f))))} :: according to XBOOLE_0:def 10,VECTSP10:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in ker (CQFunctional f) ; :: thesis:
then consider w being Vector of (VectQuot (V,(Ker f))) such that
A3: x = w and
A4: (CQFunctional f) . w = 0. K ;
w in CosetSet (V,(Ker f)) by A2;
then consider A being Coset of Ker f such that
A5: w = A ;
consider v being Vector of V such that
A6: A = v + (Ker f) by VECTSP_4:def 6;
f . v = 0. K by A1, A4, A5, A6, Def12;
then v in ker f ;
then v in Ker f by A1;
then w = zeroCoset (V,(Ker f)) by A5, A6, VECTSP_4:49
.= 0. (VectQuot (V,(Ker f))) by Th21 ;
hence x in {(0. (VectQuot (V,(Ker f))))} by A3, TARSKI:def 1; :: thesis:

end;

thus {(0. (VectQuot (V,(Ker f))))} c= ker (CQFunctional f) :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {(0. (VectQuot (V,(Ker f))))} ; :: thesis:
then A7: x = 0. (VectQuot (V,(Ker f))) by TARSKI:def 1;
(CQFunctional f) . (0. (VectQuot (V,(Ker f)))) = 0. K by HAHNBAN1:def 9;
hence x in ker (CQFunctional f) by A7; :: thesis:

end;