let CNS be ComplexNormSpace; :: thesis:
let f be PartFunc of the carrier of CNS,COMPLEX; :: thesis:
let x0 be Point of CNS; :: 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 CNS st x1 in dom f & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) :: thesis:

proof

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

proof

let n be Element of NAT ; :: thesis:
0 < 1 / (n + 1) ;
then consider p being Point of CNS such that
A5: ( p in dom f & ||.(p - x0).|| < 1 / (n + 1) & not |.((f /. p) - (f /. x0)).| < r ) by A3;
take p ; :: thesis:
thus S₁[n,p] by A5; :: thesis:

end;

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

proof

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

end;

A9: now :: thesis:

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

end;

A10: now :: thesis:

let s be Real; :: thesis:
consider n being Nat such that
A11: s " < n by SEQ_4:3;
assume 0 < s ; :: thesis:
then A12: 0 < s " ;
(s ") + 0 < n + 1 by A11, XREAL_1:8;
then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76;
then A13: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; :: thesis:
let m be Nat; :: thesis:
A14: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis:
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then 1 / (m + 1) < s by A13, XXREAL_0:2;
hence ||.((s1 . m) - x0).|| < s by A6, XXREAL_0:2, A14; :: thesis:

end;

then A15: s1 is convergent by CLVECT_1:def 15;
then lim s1 = x0 by A10, CLVECT_1:def 16;
then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A15;
then consider n being Nat such that
A16: for m being Nat st n <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < r by A2, COMSEQ_2:def 6;
A17: n in NAT by ORDINAL1:def 12;
|.(((f /* s1) . n) - (f /. x0)).| < r by A16;
hence contradiction by A9, A17; :: thesis:

end;

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

now :: thesis:

let s1 be sequence of CNS; :: thesis:
assume that
A20: rng s1 c= dom f and
A21: ( s1 is convergent & lim s1 = x0 ) ; :: thesis:

A22: now :: thesis:

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider s being Real such that
A23: 0 < s and
A24: for x1 being Point of CNS st x1 in dom f & ||.(x1 - x0).|| < s holds
|.((f /. x1) - (f /. x0)).| < p by A19;
consider n being Nat such that
A25: for m being Nat st n <= m holds
||.((s1 . m) - x0).|| < s by A21, A23, CLVECT_1:def 16;
take k = n; :: thesis:
let m be Nat; :: thesis:
A26: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis:
then A27: ||.((s1 . m) - x0).|| < s by A25;
dom s1 = NAT by FUNCT_2:def 1;
then s1 . m in rng s1 by FUNCT_1:3, A26;
then |.((f /. (s1 . m)) - (f /. x0)).| < p by A20, A24, A27;
hence |.(((f /* s1) . m) - (f /. x0)).| < p by A20, FUNCT_2:109, A26; :: thesis:

end;

then f /* s1 is convergent by COMSEQ_2:def 5;
hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A22, COMSEQ_2:def 6; :: thesis:

end;

hence f is_continuous_in x0 by A18; :: thesis: