set qf = CQFunctional f;
set W = Ker f;
set qV = VectQuot V,(Ker f);
A1:
the carrier of (VectQuot V,(Ker f)) = CosetSet V,(Ker f)
by Def6;
A2:
the carrier of (Ker f) = ker f
by Def11;
thus
ker (CQFunctional f) c= {(0. (VectQuot V,(Ker f)))}
:: according to XBOOLE_0:def 10,VECTSP10:def 10 :: thesis: {(0. (VectQuot V,(Ker f)))} c= ker (CQFunctional f)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ker (CQFunctional f) or x in {(0. (VectQuot V,(Ker f)))} )
assume
x in ker (CQFunctional f)
;
:: thesis: x in {(0. (VectQuot V,(Ker f)))}
then consider w being
Vector of
(VectQuot V,(Ker f)) such that A3:
(
x = w &
(CQFunctional f) . w = 0. K )
;
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. K
by A2, A3, A4, A5, Def12;
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 Th22
;
hence
x in {(0. (VectQuot V,(Ker f)))}
by A3, TARSKI:def 1;
:: thesis: verum
end;
thus
{(0. (VectQuot V,(Ker f)))} c= ker (CQFunctional f)
:: thesis: verum