the
carrier
of
W
=
(
0.
V
)
+
W
by
RLSUB_1:44
;
then
the
carrier
of
W
is
Coset
of
W
by
RLSUB_1:def 6
;
then
the
carrier
of
W
in
CosetSet
(
V
,
W
) ;
hence
the
carrier
of
W
is
Element
of
CosetSet
(
V
,
W
) ;
:: thesis:
verum