let f be PartFunc of REAL ,REAL ; :: thesis:
let x0, g2 be Real; :: thesis:
assume A1: ( f is_Lcontinuous_in x0 & f . x0 <> g2 ) ; :: thesis:
given r being Real such that A2: ( r > 0 & [.(x0 - r),x0.] c= dom f ) ; :: thesis:
assume A3: for r1 being Real st r1 > 0 & [.(x0 - r1),x0.] c= dom f holds
ex g being Real st
( g in [.(x0 - r1),x0.] & f . g = g2 ) ; :: thesis:
defpred S₁[ Element of NAT , set ] means ( $2 in [.(x0 - (r / ($1 + 1))),x0.] & $2 in dom f & f . $2 = g2 );
A4: for n being Element of NAT ex g being Real st S₁[n,g]

let n be Element of NAT ; :: thesis:
A5: 0 <= n by NAT_1:2;
then A6: 0 < n + 1 ;
then A7: 0 < r / (n + 1) by A2, XREAL_1:141;
0 + 1 <= n + 1 by A5, XREAL_1:9;
then r / (n + 1) <= r / 1 by A2, XREAL_1:120;
then A8: x0 - r <= x0 - (r / (n + 1)) by XREAL_1:15;
x0 - (r / (n + 1)) <= x0 by A2, A6, XREAL_1:46, XREAL_1:141;
then x0 - (r / (n + 1)) in { g1 where g1 is Real : ( x0 - r <= g1 & g1 <= x0 ) } by A8;
then A9: x0 - (r / (n + 1)) in [.(x0 - r),x0.] by RCOMP_1:def 1;
x0 - r <= x0 by A2, XREAL_1:46;
then x0 in [.(x0 - r),x0.] by XXREAL_1:1;
then [.(x0 - (r / (n + 1))),x0.] c= [.(x0 - r),x0.] by A9, XXREAL_2:def 12;
then A10: [.(x0 - (r / (n + 1))),x0.] c= dom f by A2, XBOOLE_1:1;
then consider g being Real such that
A11: ( g in [.(x0 - (r / (n + 1))),x0.] & f . g = g2 ) by A3, A7;
take g ; :: thesis:
thus S₁[n,g] by A10, A11; :: thesis:

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(A4);
deffunc H₁( Element of NAT ) -> Element of REAL = x0 - (r / ($1 + 1));
consider b being Real_Sequence such that
A13: for n being Element of NAT holds b . n = H₁(n) from SEQ_1:sch 1();
reconsider d = NAT --> x0 as Real_Sequence ;
A14: ( b is convergent & lim b = x0 ) by A13, FCONT_3:13;
A16: lim d = d . 0 by SEQ_4:41
.= x0 by FUNCOP_1:13 ;

A17: now

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

end;

then A18: a is convergent by A14, A16, SEQ_2:33;
A19: lim a = x0 by A14, A16, A17, SEQ_2:34;
A20: ( rng a c= (left_open_halfline x0) /\ (dom f) & rng a c= dom f )

thus A21: rng a c= (left_open_halfline x0) /\ (dom f) :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng a ; :: thesis:
then consider n being Element of NAT such that
A22: x = a . n by FUNCT_2:190;
A23: ( a . n in [.(x0 - (r / (n + 1))),x0.] & a . n in dom f ) by A12;
then a . n in { g1 where g1 is Real : ( x0 - (r / (n + 1)) <= g1 & g1 <= x0 ) } by RCOMP_1:def 1;
then A24: ex g1 being Real st
( g1 = a . n & x0 - (r / (n + 1)) <= g1 & g1 <= x0 ) ;
a . n <> x0 by A1, A12;
then a . n < x0 by A24, XXREAL_0:1;
then a . n in { g1 where g1 is Real : g1 < x0 } ;
then a . n in left_open_halfline x0 by XXREAL_1:229;
hence x in (left_open_halfline x0) /\ (dom f) by A22, A23, XBOOLE_0:def 4; :: thesis:

end;

(left_open_halfline x0) /\ (dom f) c= dom f by XBOOLE_1:17;
hence rng a c= dom f by A21, XBOOLE_1:1; :: thesis:

end;

A25: for n being Element of NAT holds (f /* a) . n = g2

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

end;

now

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

end;

then f /* a is V8() by VALUED_0:25;
then lim (f /* a) = (f /* a) . 0 by SEQ_4:41
.= g2 by A25 ;
hence contradiction by A1, A18, A19, A20, Def1; :: thesis: