let f be PartFunc of REAL,REAL; for x0, g2 being Real st f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) holds
ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) )
let x0, g2 be Real; ( f is_Rcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) implies ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) ) )
assume that
A1:
f is_Rcontinuous_in x0
and
A2:
f . x0 <> g2
; ( for r being Real holds
( not r > 0 or not [.x0,(x0 + r).] c= dom f ) or ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) ) )
given r being Real such that A3:
r > 0
and
A4:
[.x0,(x0 + r).] c= dom f
; ex r1 being Real st
( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> g2 ) )
defpred S1[ Element of NAT , set ] means ( $2 in [.x0,(x0 + (r / ($1 + 1))).] & $2 in dom f & f . $2 = g2 );
assume A5:
for r1 being Real st r1 > 0 & [.x0,(x0 + r1).] c= dom f holds
ex g being Real st
( g in [.x0,(x0 + r1).] & f . g = g2 )
; contradiction
A6:
for n being Element of NAT ex g being Element of REAL st S1[n,g]
proof
let n be
Element of
NAT ;
ex g being Element of REAL st S1[n,g]
x0 + 0 <= x0 + r
by A3, XREAL_1:7;
then A7:
x0 in [.x0,(x0 + r).]
by XXREAL_1:1;
0 + 1
<= n + 1
by XREAL_1:7;
then
r / (n + 1) <= r / 1
by A3, XREAL_1:118;
then A8:
x0 + (r / (n + 1)) <= x0 + r
by XREAL_1:7;
x0 + 0 = x0
;
then
x0 <= x0 + (r / (n + 1))
by A3, XREAL_1:7;
then
x0 + (r / (n + 1)) in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r ) }
by A8;
then
x0 + (r / (n + 1)) in [.x0,(x0 + r).]
by RCOMP_1:def 1;
then
[.x0,(x0 + (r / (n + 1))).] c= [.x0,(x0 + r).]
by A7, XXREAL_2:def 12;
then A9:
[.x0,(x0 + (r / (n + 1))).] c= dom f
by A4;
then consider g being
Real such that A10:
(
g in [.x0,(x0 + (r / (n + 1))).] &
f . g = g2 )
by A3, A5, XREAL_1:139;
take
g
;
( g is set & g is Element of REAL & S1[n,g] )
thus
(
g is
set &
g is
Element of
REAL &
S1[
n,
g] )
by A9, A10;
verum
end;
consider a being Real_Sequence such that
A11:
for n being Element of NAT holds S1[n,a . n]
from FUNCT_2:sch 3(A6);
A12:
rng a c= (right_open_halfline x0) /\ (dom f)
A16:
(right_open_halfline x0) /\ (dom f) c= dom f
by XBOOLE_1:17;
A17:
for n being Element of NAT holds (f /* a) . n = g2
then A18: lim (f /* a) =
(f /* a) . 0
by SEQ_4:26, VALUED_0:25
.=
g2
by A17
;
deffunc H1( Nat) -> set = x0 + (r / ($1 + 1));
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set b = seq_const x0;
A19: lim (seq_const x0) =
(seq_const x0) . 0
by SEQ_4:26
.=
x0
by SEQ_1:57
;
consider d being Real_Sequence such that
A20:
for n being Nat holds d . n = H1(n)
from SEQ_1:sch 1();
( d is convergent & lim d = x0 )
by A20, FCONT_3:6;
then
( a is convergent & lim a = x0 )
by A19, A21, SEQ_2:19, SEQ_2:20;
hence
contradiction
by A1, A2, A12, A18; verum