set qf = QcFunctional f;
set W = Ker (f *');
set qV = VectQuot (V,(Ker (f *')));
set K = F_Complex ;
A1: the carrier of (Ker (f *')) = ker (f *') by VECTSP10:def 11
.= ker f by Th23 ;
A2: the carrier of (VectQuot (V,(Ker (f *')))) = CosetSet (V,(Ker (f *'))) by VECTSP10:def 6;
thus ker (QcFunctional 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 (QcFunctional f) ; :: thesis:
then consider w being Vector of (VectQuot (V,(Ker (f *')))) such that
A3: x = w and
A4: (QcFunctional f) . w = 0. F_Complex ;
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. F_Complex by A1, A4, A5, A6, VECTSP10:def 12;
then v in ker f ;
then v in Ker (f *') by A1, STRUCT_0:def 5;
then w = zeroCoset (V,(Ker (f *'))) by A5, A6, VECTSP_4:49
.= 0. (VectQuot (V,(Ker (f *')))) by VECTSP10:21 ;
hence x in {(0. (VectQuot (V,(Ker (f *')))))} by A3, TARSKI:def 1; :: thesis:

end;

thus {(0. (VectQuot (V,(Ker (f *')))))} c= ker (QcFunctional 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;
(QcFunctional f) . (0. (VectQuot (V,(Ker (f *'))))) = 0. F_Complex by HAHNBAN1:def 9;
hence x in ker (QcFunctional f) by A7; :: thesis:

end;