set qf = QcFunctional f;
set W = Ker (f *' );
set qV = VectQuot V,(Ker (f *' ));
set K = F_Complex ;
A1:
the carrier of (VectQuot V,(Ker (f *' ))) = CosetSet V,(Ker (f *' ))
by VECTSP10:def 6;
A2: the carrier of (Ker (f *' )) =
ker (f *' )
by VECTSP10:def 11
.=
ker f
by Th26
;
thus
ker (QcFunctional f) c= {(0. (VectQuot V,(Ker (f *' ))))}
:: according to XBOOLE_0:def 10,VECTSP10:def 10 :: thesis: K176(the carrier of (VectQuot V,(Ker (f *' ))),(0. (VectQuot V,(Ker (f *' ))))) c= ker (QcFunctional f)proof
let x be
set ;
:: 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 &
(QcFunctional f) . w = 0. F_Complex )
;
w in CosetSet V,
(Ker (f *' ))
by A1;
then consider A being
Coset of
Ker (f *' ) such that A4:
w = A
;
consider v being
Vector of
V such that A5:
A = v + (Ker (f *' ))
by VECTSP_4:def 6;
f . v = 0. F_Complex
by A2, A3, A4, A5, VECTSP10:def 12;
then
v in ker f
;
then
v in Ker (f *' )
by A2, STRUCT_0:def 5;
then w =
zeroCoset V,
(Ker (f *' ))
by A4, A5, VECTSP_4:64
.=
0. (VectQuot V,(Ker (f *' )))
by VECTSP10:22
;
hence
x in {(0. (VectQuot V,(Ker (f *' ))))}
by A3, TARSKI:def 1;
:: thesis: verum
end;
thus
{(0. (VectQuot V,(Ker (f *' ))))} c= ker (QcFunctional f)
:: thesis: verum