set
f
= the
V8
()
PartFunc
of
REAL
,
REAL
;
take
the
V8
()
PartFunc
of
REAL
,
REAL
;
:: thesis:
the
V8
()
PartFunc
of
REAL
,
REAL
is
continuous
thus
the
V8
()
PartFunc
of
REAL
,
REAL
is
continuous
;
:: thesis:
verum