let x0 be Complex; 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 Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let f be PartFunc of COMPLEX,COMPLEX; ( 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 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 Nat holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
; ( 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) ) ) implies f is_continuous_in x0 )
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) )
; f is_continuous_in x0
thus
x0 in dom f
by A1; CFCONT_1:def 1 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; ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )
assume that
A3:
rng s2 c= dom f
and
A4:
( s2 is convergent & lim s2 = x0 )
; ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
now ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )per cases
( ex n being Nat st
for m being Nat st n <= m holds
s2 . m = x0 or for n being Nat ex m being Nat st
( n <= m & s2 . m <> x0 ) )
;
suppose A12:
for
n being
Nat ex
m being
Nat st
(
n <= m &
s2 . m <> x0 )
;
( f /* s2 is convergent & f /. x0 = lim (f /* s2) )defpred S1[
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 S2[
set ,
set ,
set ]
means S1[$2,$3];
defpred S3[
set ]
means s2 . $1
<> x0;
ex
m1 being
Nat st
(
0 <= m1 &
s2 . m1 <> x0 )
by A12;
then A13:
ex
m being
Nat st
S3[
m]
;
consider M being
Nat such that A14:
(
S3[
M] & ( for
n being
Nat st
S3[
n] holds
M <= n ) )
from NAT_1:sch 5(A13);
reconsider M9 =
M as
Element of
NAT by ORDINAL1:def 12;
A15:
now for n being Nat ex m being Nat st
( n < m & s2 . m <> x0 )let n be
Nat;
ex m being Nat st
( n < m & s2 . m <> x0 )consider m being
Nat such that A16:
(
n + 1
<= m &
s2 . m <> x0 )
by A12;
take m =
m;
( n < m & s2 . m <> x0 )thus
(
n < m &
s2 . m <> x0 )
by A16, NAT_1:13;
verum end; A17:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S2[
n,
x,
y]
consider F being
sequence of
NAT such that A20:
(
F . 0 = M9 & ( for
n being
Nat holds
S2[
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
V42()
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 S4[
set ]
means (
s2 . $1
<> x0 & ( for
m being
Nat holds
F . m <> $1 ) );
assume
ex
n being
Nat st
S4[
n]
;
contradiction
then A25:
ex
n being
Nat st
S4[
n]
;
consider M1 being
Nat such that A26:
(
S4[
M1] & ( for
n being
Nat st
S4[
n] holds
M1 <= n ) )
from NAT_1:sch 5(A25);
defpred S5[
Nat]
means ( $1
< M1 &
s2 . $1
<> x0 & ex
m being
Nat st
F . m = $1 );
A27:
ex
n being
Nat st
S5[
n]
A28:
for
n being
Nat st
S5[
n] holds
n <= M1
;
consider MX being
Nat such that A29:
(
S5[
MX] & ( for
n being
Nat st
S5[
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 )
;
contradiction
hence
contradiction
;
verum
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;
hence
contradiction
by A26;
verum
end; defpred S4[
Nat]
means (s2 * F) . $1
<> x0;
A36:
for
k being
Nat st
S4[
k] holds
S4[
k + 1]
proof
let k be
Nat;
( S4[k] implies S4[k + 1] )
assume
(s2 * F) . k <> x0
;
S4[k + 1]
S1[
F . k,
F . (k + 1)]
by A20;
then
s2 . (F . (k + 1)) <> x0
;
hence
S4[
k + 1]
by FUNCT_2:15;
verum
end; A37:
S4[
0 ]
by A14, A20, FUNCT_2:15;
A38:
for
n being
Nat holds
S4[
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 for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s2) . m) - (f /. x0)).| < plet p be
Real;
( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s2) . b5) - (f /. x0)).| < b3 )assume A42:
0 < p
;
ex k being Nat st
for m being Nat st k <= m holds
|.(((f /* s2) . b5) - (f /. x0)).| < b3then 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;
for m being Nat st k <= m holds
|.(((f /* s2) . b4) - (f /. x0)).| < b2let m be
Nat;
( k <= m implies |.(((f /* s2) . b3) - (f /. x0)).| < b1 )assume A44:
k <= m
;
|.(((f /* s2) . b3) - (f /. x0)).| < b1per cases
( s2 . m = x0 or s2 . m <> x0 )
;
suppose
s2 . m <> x0
;
|.(((f /* s2) . b3) - (f /. x0)).| < b1then 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;
verum end; end; end; hence
f /* s2 is
convergent
;
f /. x0 = lim (f /* s2)hence
f /. x0 = lim (f /* s2)
by A41, COMSEQ_2:def 6;
verum end; end; end;
hence
( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
; verum