let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for f being PartFunc of CNS,RNS
for x0 being Point of CNS st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let RNS be RealNormSpace; :: thesis: for f being PartFunc of CNS,RNS
for x0 being Point of CNS st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let f be PartFunc of CNS,RNS; :: thesis: for x0 being Point of CNS st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds
f is_continuous_in x0
let x0 be Point of CNS; :: thesis: ( x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
assume A1: x0 in dom f ; :: thesis: ( for N being Neighbourhood of x0 holds not (dom f) /\ N = {x0} or f is_continuous_in x0 )
given N being Neighbourhood of x0 such that A2: (dom f) /\ N = {x0} ; :: thesis: f is_continuous_in x0

now :: thesis: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1

let N1 be Neighbourhood of f /. x0; :: thesis: ex N being Neighbourhood of x0 st f .: N c= N1
take N = N; :: thesis: f .: N c= N1
A3: f /. x0 in N1 by NFCONT_1:4;
f .: N = Im (f,x0) by A2, RELAT_1:112
.= {(f . x0)} by A1, FUNCT_1:59
.= {(f /. x0)} by A1, PARTFUN1:def 6 ;
hence f .: N c= N1 by A3, ZFMISC_1:31; :: thesis: verum

end;

hence f is_continuous_in x0 by A1, Th18; :: thesis: verum