let f be PartFunc of REAL ,REAL ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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 S₁[ 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 ) ; :: thesis: contradiction
A6: for n being Element of NAT ex g being Real st S₁[n,g]

proof

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
x0 + 0 <= x0 + r by A3, XREAL_1:9;
then A7: x0 in [.x0,(x0 + r).] by XXREAL_1:1;
A8: 0 <= n by NAT_1:2;
then 0 + 1 <= n + 1 by XREAL_1:9;
then r / (n + 1) <= r / 1 by A3, XREAL_1:120;
then A9: x0 + (r / (n + 1)) <= x0 + r by XREAL_1:9;
x0 + 0 = x0 ;
then x0 <= x0 + (r / (n + 1)) by A3, A8, XREAL_1:9;
then x0 + (r / (n + 1)) in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + r ) } by A9;
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 A10: [.x0,(x0 + (r / (n + 1))).] c= dom f by A4, XBOOLE_1:1;
then consider g being Real such that
A11: ( g in [.x0,(x0 + (r / (n + 1))).] & f . g = g2 ) by A3, A5, A8, XREAL_1:141;
take g ; :: thesis: S₁[n,g]
thus S₁[n,g] by A10, A11; :: thesis: verum

end;

consider a being Real_Sequence such that
A12: for n being Element of NAT holds S₁[n,a . n] from FUNCT_2:sch 3(A6);
A13: rng a c= (right_open_halfline x0) /\ (dom f)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in (right_open_halfline x0) /\ (dom f) )
assume x in rng a ; :: thesis: x in (right_open_halfline x0) /\ (dom f)
then consider n being Element of NAT such that
A14: x = a . n by FUNCT_2:190;
a . n in [.x0,(x0 + (r / (n + 1))).] by A12;
then a . n in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) } by RCOMP_1:def 1;
then A15: ex g1 being Real st
( g1 = a . n & x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) ;
x0 <> a . n by A2, A12;
then x0 < a . n by A15, XXREAL_0:1;
then a . n in { g1 where g1 is Real : x0 < g1 } ;
then A16: a . n in right_open_halfline x0 by XXREAL_1:230;
a . n in dom f by A12;
hence x in (right_open_halfline x0) /\ (dom f) by A14, A16, XBOOLE_0:def 4; :: thesis: verum

end;

A17: (right_open_halfline x0) /\ (dom f) c= dom f by XBOOLE_1:17;
A18: for n being Element of NAT holds (f /* a) . n = g2

proof

let n be Element of NAT ; :: thesis: (f /* a) . n = g2
thus g2 = f . (a . n) by A12
.= (f /* a) . n by A13, A17, FUNCT_2:185, XBOOLE_1:1 ; :: thesis: verum

end;

now

let n be Nat; :: thesis: (f /* a) . n = (f /* a) . (n + 1)
n in NAT by ORDINAL1:def 13;
then (f /* a) . n = g2 by A18;
hence (f /* a) . n = (f /* a) . (n + 1) by A18; :: thesis: verum

end;

then A19: lim (f /* a) = (f /* a) . 0 by SEQ_4:41, VALUED_0:25
.= g2 by A18 ;
deffunc H₁( Element of NAT ) -> Element of REAL = x0 + (r / ($1 + 1));
reconsider b = NAT --> x0 as Real_Sequence ;
A20: lim b = b . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;
consider d being Real_Sequence such that
A21: for n being Element of NAT holds d . n = H₁(n) from SEQ_1:sch 1();

A22: now

let n be Element of NAT ; :: thesis: ( b . n <= a . n & a . n <= d . n )
a . n in [.x0,(x0 + (r / (n + 1))).] by A12;
then a . n in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) } by RCOMP_1:def 1;
then ex g1 being Real st
( g1 = a . n & x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) ;
hence ( b . n <= a . n & a . n <= d . n ) by A21, FUNCOP_1:13; :: thesis: verum

end;

( d is convergent & lim d = x0 ) by A21, FCONT_3:14;
then ( a is convergent & lim a = x0 ) by A20, A22, SEQ_2:33, SEQ_2:34;
hence contradiction by A1, A2, A13, A19, Def2; :: thesis: verum