let x0 be Complex; :: thesis:
let f be PartFunc of COMPLEX,COMPLEX; :: thesis:
thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) ; :: thesis:
assume that
A1: x0 in dom f and
A2: for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ; :: thesis:
thus x0 in dom f by A1; :: according to CFCONT_1:def 1 :: thesis:
let s2 be Complex_Sequence; :: thesis:
assume that
A3: rng s2 c= dom f and
A4: ( s2 is convergent & lim s2 = x0 ) ; :: thesis:

suppose ex n being Nat st
for m being Nat st n <= m holds
s2 . m = x0 ; :: thesis:

then consider N being Nat such that
A5: for m being Nat st N <= m holds
s2 . m = x0 ;
A6: for n being Nat holds (s2 ^\ N) . n = x0

proof

let n be Nat; :: thesis:
s2 . (n + N) = x0 by A5, NAT_1:12;
hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis:

end;

A7: f /* (s2 ^\ N) = (f /* s2) ^\ N by A3, VALUED_0:27;
A8: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;

A9: now :: thesis:

let p be Real; :: thesis:
assume A10: p > 0 ; :: thesis:
reconsider n = 0 as Nat ;
take n = n; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
m in NAT by ORDINAL1:def 12;
then |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| = |.((f /. ((s2 ^\ N) . m)) - (f /. x0)).| by A3, A8, FUNCT_2:109, XBOOLE_1:1
.= |.((f /. x0) - (f /. x0)).| by A6
.= 0 by COMPLEX1:44 ;
hence |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p by A10; :: thesis:

end;

then A11: f /* (s2 ^\ N) is convergent ;
then f /. x0 = lim ((f /* s2) ^\ N) by A9, A7, COMSEQ_2:def 6;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A11, A7, Th18, Th22; :: thesis:

end;

suppose A12: for n being Nat ex m being Nat st
( n <= m & s2 . m <> x0 ) ; :: thesis:

defpred S₁[ set , set ] means for n, m being Nat st $1 = n & $2 = m holds
( n < m & s2 . m <> x0 & ( for k being Nat st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S₂[ set , set , set ] means S₁[$2,$3];
defpred S₃[ set ] means s2 . $1 <> x0;
ex m1 being Nat st
( 0 <= m1 & s2 . m1 <> x0 ) by A12;
then A13: ex m being Nat st S₃[m] ;
consider M being Nat such that
A14: ( S₃[M] & ( for n being Nat st S₃[n] holds
M <= n ) ) from NAT_1:sch 5(A13);
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

A15: now :: thesis:

let n be Nat; :: thesis:
consider m being Nat such that
A16: ( n + 1 <= m & s2 . m <> x0 ) by A12;
take m = m; :: thesis:
thus ( n < m & s2 . m <> x0 ) by A16, NAT_1:13; :: thesis:

end;

A17: for n being Nat
for x being Element of NAT ex y being Element of NAT st S₂[n,x,y]

proof

let n be Nat; :: thesis:
let x be Element of NAT ; :: thesis:
defpred S₄[ Nat] means ( x < $1 & s2 . $1 <> x0 );
ex m being Nat st S₄[m] by A15;
then A18: ex m being Nat st S₄[m] ;
consider l being Nat such that
A19: ( S₄[l] & ( for k being Nat st S₄[k] holds
l <= k ) ) from NAT_1:sch 5(A18);
take l ; :: thesis:
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S₂[n,x,l] ) by A19; :: thesis:

end;

consider F being sequence of NAT such that
A20: ( F . 0 = M9 & ( for n being Nat holds S₂[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A17);
A21: for n being Nat holds F . n is real ;
dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A21, SEQ_1:2;
for n being Nat holds F . n < F . (n + 1) by A20;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;
A22: s2 * F is subsequence of s2 by VALUED_0:def 17;
then A23: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A4, Th17, Th18;
A24: for n being Nat st s2 . n <> x0 holds
ex m being Nat st F . m = n

proof

defpred S₄[ set ] means ( s2 . $1 <> x0 & ( for m being Nat holds F . m <> $1 ) );
assume ex n being Nat st S₄[n] ; :: thesis:
then A25: ex n being Nat st S₄[n] ;
consider M1 being Nat such that
A26: ( S₄[M1] & ( for n being Nat st S₄[n] holds
M1 <= n ) ) from NAT_1:sch 5(A25);
defpred S₅[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Nat st F . m = $1 );
A27: ex n being Nat st S₅[n]

proof

take M ; :: thesis:
( M <= M1 & M <> M1 ) by A14, A20, A26;
hence M < M1 by XXREAL_0:1; :: thesis:
thus s2 . M <> x0 by A14; :: thesis:
take 0 ; :: thesis:
thus F . 0 = M by A20; :: thesis:

end;

A28: for n being Nat st S₅[n] holds
n <= M1 ;
consider MX being Nat such that
A29: ( S₅[MX] & ( for n being Nat st S₅[n] holds
n <= MX ) ) from NAT_1:sch 6(A28, A27);
A30: for k being Nat st MX < k & k < M1 holds
s2 . k = x0

proof

given k being Nat such that A31: MX < k and
A32: ( k < M1 & s2 . k <> x0 ) ; :: thesis:

now :: thesis:

per cases ;

suppose ex m being Nat st F . m = k ; :: thesis:

hence contradiction by A29, A31, A32; :: thesis:

end;

suppose for m being Nat holds F . m <> k ; :: thesis:

hence contradiction by A26, A32; :: thesis:

end;

hence contradiction ; :: thesis:

end;

consider m being Nat such that
A33: F . m = MX by A29;
A34: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A20, A33;
A35: F . (m + 1) <= M1 by A20, A26, A29, A33;

now :: thesis:

assume F . (m + 1) <> M1 ; :: thesis:
then F . (m + 1) < M1 by A35, XXREAL_0:1;
hence contradiction by A30, A34; :: thesis:

end;

hence contradiction by A26; :: thesis:

end;

defpred S₄[ Nat] means (s2 * F) . $1 <> x0;
A36: for k being Nat st S₄[k] holds
S₄[k + 1]

proof

let k be Nat; :: thesis:
assume (s2 * F) . k <> x0 ; :: thesis:
S₁[F . k,F . (k + 1)] by A20;
then s2 . (F . (k + 1)) <> x0 ;
hence S₄[k + 1] by FUNCT_2:15; :: thesis:

end;

A37: S₄[ 0 ] by A14, A20, FUNCT_2:15;
A38: for n being Nat holds S₄[n] from NAT_1:sch 2(A37, A36);
A39: rng (s2 * F) c= rng s2 by A22, VALUED_0:21;
then rng (s2 * F) c= dom f by A3;
then A40: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A2, A38, A23;

A41: now :: thesis:

let p be Real; :: thesis:
assume A42: 0 < p ; :: thesis:
then consider n being Nat such that
A43: for m being Nat st n <= m holds
|.(((f /* (s2 * F)) . m) - (f /. x0)).| < p by A40, COMSEQ_2:def 6;
reconsider k = F . n as Nat ;
take k = k; :: thesis:
let m be Nat; :: thesis:
assume A44: k <= m ; :: thesis:

per cases ;

suppose A45: s2 . m = x0 ; :: thesis:

m in NAT by ORDINAL1:def 12;
then |.(((f /* s2) . m) - (f /. x0)).| = |.((f /. x0) - (f /. x0)).| by A3, FUNCT_2:109, A45
.= 0 by COMPLEX1:44 ;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A42; :: thesis:

end;

suppose s2 . m <> x0 ; :: thesis:

then consider l being Nat such that
A46: m = F . l by A24;
A47: l in NAT by ORDINAL1:def 12;
A48: m in NAT by ORDINAL1:def 12;
n <= l by A44, A46, SEQM_3:1;
then |.(((f /* (s2 * F)) . l) - (f /. x0)).| < p by A43;
then |.((f /. ((s2 * F) . l)) - (f /. x0)).| < p by A3, A39, FUNCT_2:109, XBOOLE_1:1, A47;
then |.((f /. (s2 . m)) - (f /. x0)).| < p by A46, FUNCT_2:15, A47;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A3, FUNCT_2:109, A48; :: thesis:

end;

hence f /* s2 is convergent ; :: thesis:
hence f /. x0 = lim (f /* s2) by A41, COMSEQ_2:def 6; :: thesis:

end;

hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) ; :: thesis: