let
X
be
RealNormSpace
;
:: thesis:
the
carrier
of
X
-->
0
=
0.
(
DualSp
X
)
the
carrier
of
X
-->
0
=
0.
(
R_VectorSpace_of_BoundedLinearFunctionals
X
)
by
Th26
.=
0.
(
DualSp
X
)
;
hence
the
carrier
of
X
-->
0
=
0.
(
DualSp
X
)
;
:: thesis:
verum