let x0 be real number ; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_continuous_in x0 iff for s1 being Real_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 REAL,REAL; :: thesis: ( f is_continuous_in x0 iff for s1 being Real_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 for s1 being Real_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 Def1; :: thesis: ( ( for s1 being Real_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: for s1 being Real_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
let s2 be Real_Sequence; :: according to FCONT_1:def 1 :: thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) )
assume that
A2: rng s2 c= dom f and
A3: ( 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
A4: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A5: 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 A4, NAT_1:12;
hence (s2 ^\ N) . n = x0 by NAT_1:def 3; :: thesis: verum
end;
A6: f /* (s2 ^\ N) = (f /* s2) ^\ N by A2, VALUED_0:27;
A7: rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
A8: now
let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p )
assume A9: p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p )
assume n <= m ; :: thesis: abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p
abs (((f /* (s2 ^\ N)) . m) - (f . x0)) = abs ((f . ((s2 ^\ N) . m)) - (f . x0)) by A2, A7, FUNCT_2:185, XBOOLE_1:1
.= abs ((f . x0) - (f . x0)) by A5
.= 0 by ABSVALUE:7 ;
hence abs (((f /* (s2 ^\ N)) . m) - (f . x0)) < p by A9; :: thesis: verum
end;
then A10: f /* (s2 ^\ N) is convergent by SEQ_2:def 6;
then f . x0 = lim ((f /* s2) ^\ N) by A8, A6, SEQ_2:def 7;
hence ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) by A10, A6, SEQ_4:33, SEQ_4:35; :: thesis: verum
end;
suppose A11: 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) )
defpred S1[ Element of NAT , set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S2[ set ] means s2 . $1 <> x0;
ex m1 being Element of NAT st
( 0 <= m1 & s2 . m1 <> x0 ) by A11;
then A12: ex m being Nat st S2[m] ;
consider M being Nat such that
A13: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from NAT_1:sch 5(A12);
reconsider M9 = M as Element of NAT by ORDINAL1:def 13;
A14: 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
A15: ( n + 1 <= m & s2 . m <> x0 ) by A11;
take m = m; :: thesis: ( n < m & s2 . m <> x0 )
thus ( n < m & s2 . m <> x0 ) by A15, NAT_1:13; :: thesis: verum
end;
A16: for n, x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n, x be Element of NAT ; :: thesis: ex y being Element of NAT st S1[n,x,y]
defpred S3[ Nat] means ( x < $1 & s2 . $1 <> x0 );
ex m being Element of NAT st S3[m] by A14;
then A17: ex m being Nat st S3[m] ;
consider l being Nat such that
A18: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch 5(A17);
 take l ; :: thesis: ( l is Element of REAL & l is Element of NAT & S1[n,x,l] )
l in NAT by ORDINAL1:def 13;
hence ( l is Element of REAL & l is Element of NAT & S1[n,x,l] ) by A18; :: thesis: verum
end;
consider F being Function of NAT,NAT such that
A19: ( F . 0 = M9 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A16);
A20: rng F c= REAL by XBOOLE_1:1;
A21: rng F c= NAT ;
A22: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A20, RELSET_1:11;
A23: now
let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A22, FUNCT_1:def 5;
hence F . n is Element of NAT by A21; :: 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 A23;
hence F . n < F . (n + 1) by A19; :: thesis: verum
end;
then reconsider F = F as V38() sequence of NAT by SEQM_3:def 11;
A24: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A3, SEQ_4:29, SEQ_4:30;
A25: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ set ] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S3[n] ; :: thesis: contradiction
then A26: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A27: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch 5(A26);
 defpred S4[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );
A28: ex n being Nat st S4[n]
proof
take M ; :: thesis: S4[M]
( M <= M1 & M <> M1 ) by A13, A19, A27;
hence M < M1 by XXREAL_0:1; :: thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus s2 . M <> x0 by A13; :: thesis: ex m being Element of NAT st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A19; :: thesis: verum
end;
A29: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A30: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from NAT_1:sch 6(A29, A28);
 A31: for k being Element of NAT st MX < k & k < M1 holds
s2 . k = x0
proof
given k being Element of NAT such that A32: MX < k and
A33: ( 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 ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A34: F . m = MX by A30;
A35: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A19, A34;
M1 in NAT by ORDINAL1:def 13;
then A36: F . (m + 1) <= M1 by A19, A27, A30, A34;
now
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A36, XXREAL_0:1;
hence contradiction by A31, A35; :: thesis: verum
end;
hence contradiction by A27; :: thesis: verum
end;
A37: for n being Element of NAT holds (s2 * F) . n <> x0
proof
defpred S3[ Element of NAT ] means (s2 * F) . $1 <> x0;
A38: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S3[k] implies S3[k + 1] )
assume (s2 * F) . k <> x0 ; :: thesis: S3[k + 1]
S1[k,F . k,F . (k + 1)] by A19;
then s2 . (F . (k + 1)) <> x0 ;
hence S3[k + 1] by FUNCT_2:21; :: thesis: verum
end;
A39: S3[ 0 ] by A13, A19, FUNCT_2:21;
thus for n being Element of NAT holds S3[n] from NAT_1:sch 1(A39, A38); :: thesis: verum
end;
A40: rng (s2 * F) c= rng s2 by VALUED_0:21;
then rng (s2 * F) c= dom f by A2, XBOOLE_1:1;
then A41: ( f /* (s2 * F) is convergent & f . x0 = lim (f /* (s2 * F)) ) by A1, A37, A24;
A42: now
let p be real number ; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p )
assume A43: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p
then consider n being Element of NAT such that
A44: for m being Element of NAT st n <= m holds
abs (((f /* (s2 * F)) . m) - (f . x0)) < p by A41, SEQ_2:def 7;
take k = F . n; :: thesis: for m being Element of NAT st k <= m holds
abs (((f /* s2) . m) - (f . x0)) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((f /* s2) . m) - (f . x0)) < p )
assume A45: k <= m ; :: thesis: abs (((f /* s2) . m) - (f . x0)) < p
now
per cases ( s2 . m = x0 or s2 . m <> x0 ) ;
suppose s2 . m = x0 ; :: thesis: abs (((f /* s2) . m) - (f . x0)) < p
then abs (((f /* s2) . m) - (f . x0)) = abs ((f . x0) - (f . x0)) by A2, FUNCT_2:185
.= 0 by ABSVALUE:7 ;
hence abs (((f /* s2) . m) - (f . x0)) < p by A43; :: thesis: verum
end;
suppose s2 . m <> x0 ; :: thesis: abs (((f /* s2) . m) - (f . x0)) < p
then consider l being Element of NAT such that
A46: m = F . l by A25;
n <= l by A45, A46, SEQM_3:7;
then abs (((f /* (s2 * F)) . l) - (f . x0)) < p by A44;
then abs ((f . ((s2 * F) . l)) - (f . x0)) < p by A2, A40, FUNCT_2:185, XBOOLE_1:1;
then abs ((f . (s2 . m)) - (f . x0)) < p by A46, FUNCT_2:21;
hence abs (((f /* s2) . m) - (f . x0)) < p by A2, FUNCT_2:185; :: thesis: verum
end;
end;
end;
hence abs (((f /* s2) . m) - (f . x0)) < p ; :: thesis: verum
end;
hence f /* s2 is convergent by SEQ_2:def 6; :: thesis: f . x0 = lim (f /* s2)
hence f . x0 = lim (f /* s2) by A42, SEQ_2:def 7; :: thesis: verum
end;
end;
end;
hence ( f /* s2 is convergent & f . x0 = lim (f /* s2) ) ; :: thesis: verum