let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds
f is_continuous_on dom f
let RNS be RealNormSpace; :: thesis: for f being PartFunc of RNS,CNS st ex r being Point of CNS st rng f = {r} holds
f is_continuous_on dom f
let f be PartFunc of RNS,CNS; :: thesis: ( ex r being Point of CNS st rng f = {r} implies f is_continuous_on dom f )
given r being Point of CNS such that A1: rng f = {r} ; :: thesis: f is_continuous_on dom f

now

let x1, x2 be Point of RNS; :: thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| )
assume A2: ( x1 in dom f & x2 in dom f ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).||
then ( f . x1 in rng f & f . x2 in rng f ) by FUNCT_1:def 5;
then ( f /. x1 in rng f & f /. x2 in rng f ) by A2, PARTFUN1:def 8;
then ( f /. x1 = r & f /. x2 = r ) by A1, TARSKI:def 1;
then ||.((f /. x1) - (f /. x2)).|| = ||.(0. CNS).|| by RLVECT_1:28
.= 0 by CLVECT_1:103 ;
hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by NORMSP_1:8; :: thesis: verum

end;

then f is_Lipschitzian_on dom f by Def29;
hence f is_continuous_on dom f by Th139; :: thesis: verum