A1
: the
carrier
of
F_Complex
=
COMPLEX
by
COMPLFLD:def 1
;
then
reconsider
f
=
f
as
Function
of
V
,
COMPLEX
;
f
*'
is
Function
of
V
,
COMPLEX
;
hence
f
*'
is
Functional
of
V
by
A1
;
:: thesis:
verum