let CNS1, CNS2 be ComplexNormSpace; :: thesis:
let f be PartFunc of CNS1,CNS2; :: thesis:
let x0 be Point of CNS1; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) :: thesis:

proof

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f by Def15; :: thesis:
let N1 be Neighbourhood of f /. x0; :: thesis:
consider N being Neighbourhood of x0 such that
A2: for x1 being Point of CNS1 st x1 in dom f & x1 in N holds
f /. x1 in N1 by A1, Th35;
take N ; :: thesis:

now

let r be set ; :: thesis:
assume r in f .: N ; :: thesis:
then consider x being Point of CNS1 such that
A3: x in dom f and
A4: ( x in N & r = f . x ) by PARTFUN2:78;
( x in dom f & x in N & r = f /. x ) by A3, A4, PARTFUN1:def 8;
hence r in N1 by A2; :: thesis:

end;

hence f .: N c= N1 by TARSKI:def 3; :: thesis:

end;

assume A5: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ; :: thesis:

now

let N1 be Neighbourhood of f /. x0; :: thesis:
consider N being Neighbourhood of x0 such that
A6: f .: N c= N1 by A5;
take N = N; :: thesis:
let x1 be Point of CNS1; :: thesis:
assume A7: ( x1 in dom f & x1 in N ) ; :: thesis:
then f . x1 in f .: N by FUNCT_1:def 12;
then f . x1 in N1 by A6;
hence f /. x1 in N1 by A7, PARTFUN1:def 8; :: thesis:

end;

hence f is_continuous_in x0 by A5, Th35; :: thesis: