let CNS be ComplexNormSpace; for RNS being RealNormSpace
for f being PartFunc of CNS,RNS st f is total & ( for x1, x2 being Point of CNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS
let RNS be RealNormSpace; for f being PartFunc of CNS,RNS st f is total & ( for x1, x2 being Point of CNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS
let f be PartFunc of CNS,RNS; ( f is total & ( for x1, x2 being Point of CNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS st f is_continuous_in x0 implies f is_continuous_on the carrier of CNS )
assume that
A1:
f is total
and
A2:
for x1, x2 being Point of CNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2)
; ( for x0 being Point of CNS holds not f is_continuous_in x0 or f is_continuous_on the carrier of CNS )
A3:
dom f = the carrier of CNS
by A1, PARTFUN1:def 2;
given x0 being Point of CNS such that A4:
f is_continuous_in x0
; f is_continuous_on the carrier of CNS
(f /. x0) + (0. RNS) =
f /. x0
by RLVECT_1:4
.=
f /. (x0 + (0. CNS))
by RLVECT_1:4
.=
(f /. x0) + (f /. (0. CNS))
by A2
;
then A5:
f /. (0. CNS) = 0. RNS
by RLVECT_1:8;
A7:
now for x1, x2 being Point of CNS holds f /. (x1 - x2) = (f /. x1) - (f /. x2)end;
hence
f is_continuous_on the carrier of CNS
by A3, Th45; verum