take
the
empty
PartFunc
of
REAL
,
(
REAL
n
)
;
:: thesis:
the
empty
PartFunc
of
REAL
,
(
REAL
n
)
is
empty
thus
the
empty
PartFunc
of
REAL
,
(
REAL
n
)
is
empty
;
:: thesis:
verum