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: K160( the carrier of (VectQuot (V,(Ker (f *')))),(0. (VectQuot (V,(Ker (f *')))))) c= ker (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: K160( the carrier of (VectQuot (V,(Ker (f *')))),(0. (VectQuot (V,(Ker (f *')))))) c= ker (QcFunctional f)

proof

thus
{(0. (VectQuot (V,(Ker (f *')))))} c= ker (QcFunctional f)
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ker (QcFunctional f) or x in {(0. (VectQuot (V,(Ker (f *')))))} )

assume x in ker (QcFunctional f) ; :: thesis: x in {(0. (VectQuot (V,(Ker (f *')))))}

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: verum

end;assume x in ker (QcFunctional f) ; :: thesis: x in {(0. (VectQuot (V,(Ker (f *')))))}

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: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(0. (VectQuot (V,(Ker (f *')))))} or x in ker (QcFunctional f) )

assume x in {(0. (VectQuot (V,(Ker (f *')))))} ; :: thesis: x in ker (QcFunctional f)

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: verum

end;assume x in {(0. (VectQuot (V,(Ker (f *')))))} ; :: thesis: x in ker (QcFunctional f)

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: verum