let x0 be Element of COMPLEX ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX holds
( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) by Def2; :: thesis: ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume A1: ( x0 in dom f & ( for s1 being Complex_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ; :: thesis: f is_continuous_in x0
hence x0 in dom f ; :: according to CFCONT_1:def 2 :: 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 s2 be Complex_Sequence; :: thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )
assume A2: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 ) ; :: thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )

now

per cases ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ) ;

suppose ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 ; :: thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )

then consider N being Element of NAT such that
A3: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A4: for n being Element of NAT holds (s2 ^\ N) . n = x0

proof

let n be Element of NAT ; :: thesis: (s2 ^\ N) . n = x0
s2 . (n + N) = x0 by A3, NAT_1:12;
hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis: verum

end;

A5: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;

A6: now

let p be Real; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p )
assume A7: p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p )
assume n <= m ; :: thesis: |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p
|.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| = |.((f /. ((s2 ^\ N) . m)) - (f /. x0)).| by A2, A5, FUNCT_2:186, XBOOLE_1:1
.= |.((f /. x0) - (f /. x0)).| by A4
.= 0 by COMPLEX1:130 ;
hence |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p by A7; :: thesis: verum

end;

then A8: f /* (s2 ^\ N) is convergent by COMSEQ_2:def 4;
f /* (s2 ^\ N) = (f /* s2) ^\ N by A2, VALUED_0:27;
then ( f /* s2 is convergent & f /. x0 = lim ((f /* s2) ^\ N) ) by A6, A8, Th44, COMSEQ_2:def 5;
hence ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by Th43; :: thesis: verum

end;

suppose A9: for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ; :: thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )

then consider m1 being Element of NAT such that
A10: ( 0 <= m1 & s2 . m1 <> x0 ) ;
defpred S₁[ set ] means s2 . $1 <> x0;
A11: ex m being Nat st S₁[m] by A10;
consider M being Nat such that
A12: ( S₁[M] & ( for n being Nat st S₁[n] holds
M <= n ) ) from NAT_1:sch 5(A11);

A13: now

let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & s2 . m <> x0 )
consider m being Element of NAT such that
A14: ( n + 1 <= m & s2 . m <> x0 ) by A9;
take m = m; :: thesis: ( n < m & s2 . m <> x0 )
thus ( n < m & s2 . m <> x0 ) by A14, NAT_1:13; :: thesis: verum

end;

defpred S₂[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S₃[ set , set , set ] means S₂[$2,$3];
A15: for n, x being Element of NAT ex y being Element of NAT st S₃[n,x,y]

proof

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

end;

reconsider M' = M as Element of NAT by ORDINAL1:def 13;
consider F being Function of NAT ,NAT such that
A18: ( F . 0 = M' & ( for n being Element of NAT holds S₃[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A15);
A19: ( dom F = NAT & rng F c= NAT ) by FUNCT_2:def 1;
for n being Element of NAT holds F . n is real ;
then reconsider F = F as Real_Sequence by A19, SEQ_1:4;

A20: now

let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A19, FUNCT_1:def 5;
hence F . n is Element of NAT by A19; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: F . n < F . (n + 1)
( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A20;
hence F . n < F . (n + 1) by A18; :: thesis: verum

end;

then reconsider F = F as V35() sequence of NAT by SEQM_3:def 11;
A21: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n

proof

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

proof

take M ; :: thesis: S₅[M]
A25: M <= M1 by A12, A23;
M <> M1 by A18, A23;
hence M < M1 by A25, XXREAL_0:1; :: thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus s2 . M <> x0 by A12; :: thesis: ex m being Element of NAT st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A18; :: thesis: verum

end;

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

proof

given k being Element of NAT such that A29: ( MX < k & k < M1 & s2 . k <> x0 ) ; :: thesis: contradiction

now

per cases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;

suppose ex m being Element of NAT st F . m = k ; :: thesis: contradiction

hence contradiction by A27, A29; :: thesis: verum

end;

suppose for m being Element of NAT holds F . m <> k ; :: thesis: contradiction

hence contradiction by A23, A29; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

consider m being Element of NAT such that
A30: F . m = MX by A27;
A31: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 & ( for k being Element of NAT st MX < k & s2 . k <> x0 holds
F . (m + 1) <= k ) ) by A18, A30;
M1 in NAT by ORDINAL1:def 13;
then A32: F . (m + 1) <= M1 by A18, A23, A27, A30;

now

assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A32, XXREAL_0:1;
hence contradiction by A28, A31; :: thesis: verum

end;

hence contradiction by A23; :: thesis: verum

end;

defpred S₄[ Element of NAT ] means (s2 * F) . $1 <> x0;
A33: S₄[ 0 ] by A12, A18, FUNCT_2:21;
A34: for k being Element of NAT st S₄[k] holds
S₄[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₄[k] implies S₄[k + 1] )
assume (s2 * F) . k <> x0 ; :: thesis: S₄[k + 1]
S₂[F . k,F . (k + 1)] by A18;
then s2 . (F . (k + 1)) <> x0 ;
hence S₄[k + 1] by FUNCT_2:21; :: thesis: verum

end;

A35: for n being Element of NAT holds S₄[n] from NAT_1:sch 1(A33, A34);
A36: s2 * F is subsequence of s2 by VALUED_0:def 17;
then A37: s2 * F is convergent by A2, Th39;
A38: rng (s2 * F) c= rng s2 by A36, VALUED_0:21;
then A39: rng (s2 * F) c= dom f by A2, XBOOLE_1:1;
lim (s2 * F) = x0 by A2, A36, Th40;
then A40: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A1, A35, A37, A39;

A41: now

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

now

per cases ( s2 . m = x0 or s2 . m <> x0 ) ;

suppose s2 . m = x0 ; :: thesis: |.(((f /* s2) . m) - (f /. x0)).| < p

then |.(((f /* s2) . m) - (f /. x0)).| = |.((f /. x0) - (f /. x0)).| by A2, FUNCT_2:186
.= 0 by COMPLEX1:130 ;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A42; :: thesis: verum

end;

suppose s2 . m <> x0 ; :: thesis: |.(((f /* s2) . m) - (f /. x0)).| < p

then consider l being Element of NAT such that
A45: m = F . l by A21;
n <= l by A44, A45, SEQM_3:7;
then |.(((f /* (s2 * F)) . l) - (f /. x0)).| < p by A43;
then |.((f /. ((s2 * F) . l)) - (f /. x0)).| < p by A2, A38, FUNCT_2:186, XBOOLE_1:1;
then |.((f /. (s2 . m)) - (f /. x0)).| < p by A45, FUNCT_2:21;
hence |.(((f /* s2) . m) - (f /. x0)).| < p by A2, FUNCT_2:186; :: thesis: verum

end;

end;

end;

hence |.(((f /* s2) . m) - (f /. x0)).| < p ; :: thesis: verum

end;

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

end;

end;

end;

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