let x0 be Complex; :: thesis: for f being PartFunc of COMPLEX,COMPLEX holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) )
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 Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) :: thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 )

proof

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

proof

let n be Nat; :: thesis: ex g being Complex st S₁[n,g]
0 < 1 / (n + 1) ;
then consider g being Complex such that
A5: ( g in dom f & |.(g - x0).| < 1 / (n + 1) & not |.((f /. g) - (f /. x0)).| < r ) by A3;
take g ; :: thesis: S₁[n,g]
thus S₁[n,g] by A5; :: thesis: verum

end;

consider s1 being Complex_Sequence such that
A6: for n being Nat holds S₁[n,s1 . n] from CFCONT_1:sch 1(A4);
A7: rng s1 c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng s1 or x in dom f )
assume x in rng s1 ; :: thesis: x in dom f
then ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence x in dom f by A6; :: thesis: verum

end;

A8: now :: thesis: for n being Nat holds not |.(((f /* s1) . n) - (f /. x0)).| < r

let n be Nat; :: thesis: not |.(((f /* s1) . n) - (f /. x0)).| < r
A9: n in NAT by ORDINAL1:def 12;
not |.((f /. (s1 . n)) - (f /. x0)).| < r by A6;
hence not |.(((f /* s1) . n) - (f /. x0)).| < r by A7, FUNCT_2:109, A9; :: thesis: verum

end;

A10: now :: thesis: for s being Real st 0 < s holds
ex k being Nat st
for m being Nat st k <= m holds
|.((s1 . m) - x0).| < s

let s be Real; :: thesis: ( 0 < s implies ex k being Nat st
for m being Nat st k <= m holds
|.((s1 . m) - x0).| < s )
consider n being Nat such that
A11: s " < n by SEQ_4:3;
assume 0 < s ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((s1 . m) - x0).| < s
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: for m being Nat st k <= m holds
|.((s1 . m) - x0).| < s
let m be Nat; :: thesis: ( k <= m implies |.((s1 . m) - x0).| < s )
assume k <= m ; :: thesis: |.((s1 . m) - x0).| < s
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; :: thesis: verum

end;

then A14: s1 is convergent ;
then lim s1 = x0 by A10, COMSEQ_2:def 6;
then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A14;
then consider n being Nat such that
A15: for m being Nat st n <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < r by A2, COMSEQ_2:def 6;
|.(((f /* s1) . n) - (f /. x0)).| < r by A15;
hence contradiction by A8; :: thesis: verum

end;

assume that
A16: x0 in dom f and
A17: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) ; :: thesis: f is_continuous_in x0

now :: thesis: for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

let s1 be Complex_Sequence; :: thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A18: rng s1 c= dom f and
A19: ( s1 is convergent & lim s1 = x0 ) ; :: thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )

A20: now :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p

let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p )
assume 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p
then consider s being Real such that
A21: 0 < s and
A22: for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < p by A17;
consider n being Nat such that
A23: for m being Nat st n <= m holds
|.((s1 . m) - x0).| < s by A19, A21, COMSEQ_2:def 6;
take k = n; :: thesis: for m being Nat st k <= m holds
|.(((f /* s1) . m) - (f /. x0)).| < p
let m be Nat; :: thesis: ( k <= m implies |.(((f /* s1) . m) - (f /. x0)).| < p )
A24: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis: |.(((f /* s1) . m) - (f /. x0)).| < p
then ( s1 . m in rng s1 & |.((s1 . m) - x0).| < s ) by A23, VALUED_0:28;
then |.((f /. (s1 . m)) - (f /. x0)).| < p by A18, A22;
hence |.(((f /* s1) . m) - (f /. x0)).| < p by A18, FUNCT_2:109, A24; :: thesis: verum

end;

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

end;

hence f is_continuous_in x0 by A16; :: thesis: verum