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
for x1 being Point of CNS1 st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ) :: thesis:

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f ; :: thesis:
let N1 be Neighbourhood of f /. x0; :: thesis:
consider r being Real such that
A2: 0 < r and
A3: { y where y is Point of CNS2 : ||.(y - (f /. x0)).|| < r } c= N1 by Def1;
consider s being Real such that
A4: 0 < s and
A5: for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th8;
reconsider N = { z where z is Point of CNS1 : ||.(z - x0).|| < s } as Neighbourhood of x0 by A4, Th2;
take N ; :: thesis:
let x1 be Point of CNS1; :: thesis:
assume that
A6: x1 in dom f and
A7: x1 in N ; :: thesis:
ex z being Point of CNS1 st
( x1 = z & ||.(z - x0).|| < s ) by A7;
then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;
then f /. x1 in { y where y is Point of CNS2 : ||.(y - (f /. x0)).|| < r } ;
hence f /. x1 in N1 by A3; :: thesis:

end;

assume that
A8: x0 in dom f and
A9: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being Point of CNS1 st x1 in dom f & x1 in N holds
f /. x1 in N1 ; :: thesis:

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then reconsider N1 = { y where y is Point of CNS2 : ||.(y - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by Th2;
consider N2 being Neighbourhood of x0 such that
A10: for x1 being Point of CNS1 st x1 in dom f & x1 in N2 holds
f /. x1 in N1 by A9;
consider s being Real such that
A11: 0 < s and
A12: { z where z is Point of CNS1 : ||.(z - x0).|| < s } c= N2 by Def1;
take s = s; :: thesis:
for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r

let x1 be Point of CNS1; :: thesis:
assume that
A13: x1 in dom f and
A14: ||.(x1 - x0).|| < s ; :: thesis:
x1 in { z where z is Point of CNS1 : ||.(z - x0).|| < s } by A14;
then f /. x1 in N1 by A10, A12, A13;
then ex y being Point of CNS2 st
( f /. x1 = y & ||.(y - (f /. x0)).|| < r ) ;
hence ||.((f /. x1) - (f /. x0)).|| < r ; :: thesis:

end;

hence ( 0 < s & ( for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A11; :: thesis:

end;