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 *')))))}
XBOOLE_0:def 10,VECTSP10:def 10 K160( the carrier of (VectQuot (V,(Ker (f *')))),(0. (VectQuot (V,(Ker (f *')))))) c= ker (QcFunctional f)proof
let x be
object ;
TARSKI:def 3 ( not x in ker (QcFunctional f) or x in {(0. (VectQuot (V,(Ker (f *')))))} )
assume
x in ker (QcFunctional f)
;
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;
verum
end;
thus
{(0. (VectQuot (V,(Ker (f *')))))} c= ker (QcFunctional f)
verum