reconsider
f
=
f
as
linear-Functional
of
X
by
Def9
;
f
.
v
is
Element
of
REAL
;
hence
f
.
v
is
Element
of
REAL
;
:: thesis:
verum