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 r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) :: thesis:

assume A1: f is_continuous_in x0 ; :: thesis:
hence x0 in dom f by Def15; :: thesis:
given r being Real such that A2: ( 0 < r & ( for s being Real holds
( not 0 < s or ex x1 being Point of CNS1 st
( x1 in dom f & ||.(x1 - x0).|| < s & not ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ; :: thesis:
defpred S₁[ Element of NAT , Point of CNS1] means ( $2 in dom f & ||.($2 - x0).|| < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x0)).|| < r );
A3: for n being Element of NAT ex p being Point of CNS1 st S₁[n,p]

let n be Element of NAT ; :: thesis:
0 < n + 1 by NAT_1:3;
then 0 < (n + 1) " by XREAL_1:124;
then 0 < 1 / (n + 1) by XCMPLX_1:217;
then consider p being Point of CNS1 such that
A4: ( p in dom f & ||.(p - x0).|| < 1 / (n + 1) & not ||.((f /. p) - (f /. x0)).|| < r ) by A2;
take p ; :: thesis:
thus S₁[n,p] by A4; :: thesis:

end;

consider s1 being Function of NAT ,the carrier of CNS1 such that
A5: for n being Element of NAT holds S₁[n,s1 . n] from FUNCT_2:sch 3(A3);
reconsider s1 = s1 as sequence of CNS1 ;
A6: rng s1 c= dom f

let v be set ; :: according to TARSKI:def 3 :: thesis:
assume A7: v in rng s1 ; :: thesis:
dom s1 = NAT by FUNCT_2:def 1;
then ex n being set st
( n in NAT & v = s1 . n ) by A7, FUNCT_1:def 5;
hence v in dom f by A5; :: thesis:

end;

A8: now

let n be Element of NAT ; :: thesis:
not ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A5;
hence not ||.(((f /* s1) . n) - (f /. x0)).|| < r by A6, FUNCT_2:186; :: thesis:

end;

A9: now

let s be Real; :: thesis:
assume 0 < s ; :: thesis:
then A10: 0 < s " by XREAL_1:124;
consider n being Element of NAT such that
A11: s " < n by SEQ_4:10;
take k = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A12: k <= m ; :: thesis:
(s " ) + 0 < n + 1 by A11, XREAL_1:10;
then 1 / (n + 1) < 1 / (s " ) by A10, XREAL_1:78;
then A13: 1 / (n + 1) < s by XCMPLX_1:218;
k + 1 <= m + 1 by A12, XREAL_1:8;
then 1 / (m + 1) <= 1 / (k + 1) by NAT_1:3, XREAL_1:120;
then A14: 1 / (m + 1) < s by A13, XXREAL_0:2;
||.((s1 . m) - x0).|| < 1 / (m + 1) by A5;
hence ||.((s1 . m) - x0).|| < s by A14, XXREAL_0:2; :: thesis:

end;

then A15: s1 is convergent by CLVECT_1:def 16;
then lim s1 = x0 by A9, CLVECT_1:def 18;
then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A6, A15, Def15;
then consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < r by A2, CLVECT_1:def 18;
||.(((f /* s1) . n) - (f /. x0)).|| < r by A16;
hence contradiction by A8; :: thesis:

end;

assume A17: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ; :: thesis:

let s1 be sequence of CNS1; :: thesis:
assume A18: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 ) ; :: thesis:

A19: now

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider s being Real such that
A20: ( 0 < s & ( for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < p ) ) by A17;
consider n being Element of NAT such that
A21: for m being Element of NAT st n <= m holds
||.((s1 . m) - x0).|| < s by A18, A20, CLVECT_1:def 18;
take k = n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A22: k <= m ; :: thesis:
dom s1 = NAT by FUNCT_2:def 1;
then A23: s1 . m in rng s1 by FUNCT_1:12;
||.((s1 . m) - x0).|| < s by A21, A22;
then ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A18, A20, A23;
hence ||.(((f /* s1) . m) - (f /. x0)).|| < p by A18, FUNCT_2:186; :: thesis:

end;

then f /* s1 is convergent by CLVECT_1:def 16;
hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A19, CLVECT_1:def 18; :: thesis:

end;

hence f is_continuous_in x0 by A17, Def15; :: thesis: