set
f
= the
constant
PartFunc
of
REAL
, the
carrier
of
S
;
take
the
constant
PartFunc
of
REAL
, the
carrier
of
S
;
:: thesis:
the
constant
PartFunc
of
REAL
, the
carrier
of
S
is
continuous
thus
the
constant
PartFunc
of
REAL
, the
carrier
of
S
is
continuous
;
:: thesis:
verum