let f be PartFunc of REAL,REAL; :: thesis: for x0, g2 being Real st f is_Lcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) holds
ex r1 being Real st
( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds
f . g <> g2 ) )
let x0, g2 be Real; :: thesis: ( f is_Lcontinuous_in x0 & f . x0 <> g2 & ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom f ) implies ex r1 being Real st
( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds
f . g <> g2 ) ) )
assume that
A1: f is_Lcontinuous_in x0 and
A2: f . x0 <> g2 ; :: thesis: ( for r being Real holds
( not r > 0 or not [.(x0 - r),x0.] c= dom f ) or ex r1 being Real st
( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds
f . g <> g2 ) ) )
given r being Real such that A3: r > 0 and
A4: [.(x0 - r),x0.] c= dom f ; :: thesis: ex r1 being Real st
( r1 > 0 & [.(x0 - r1),x0.] c= dom f & ( for g being Real st g in [.(x0 - r1),x0.] holds
f . g <> g2 ) )
defpred S1[ Element of NAT , set ] means ( $2 in [.(x0 - (r / ($1 + 1))),x0.] & $2 in dom f & f . $2 = g2 );
assume A5: 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: 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 ; :: thesis: ex g being Element of REAL st S1[n,g]
x0 - r <= x0 by A3, XREAL_1:44;
then A7: x0 in [.(x0 - r),x0.] 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 <= x0 - (r / (n + 1)) by XREAL_1:13;
x0 - (r / (n + 1)) <= x0 by A3, XREAL_1:44, XREAL_1:139;
then x0 - (r / (n + 1)) in { g1 where g1 is Real : ( x0 - r <= g1 & g1 <= x0 ) } by A8;
then x0 - (r / (n + 1)) in [.(x0 - r),x0.] by RCOMP_1:def 1;
then [.(x0 - (r / (n + 1))),x0.] c= [.(x0 - r),x0.] by A7, XXREAL_2:def 12;
then A9: [.(x0 - (r / (n + 1))),x0.] c= dom f by A4;
then consider g being Real such that
A10: ( g in [.(x0 - (r / (n + 1))),x0.] & f . g = g2 ) by A3, A5, XREAL_1:139;
take g ; :: thesis: ( 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; :: thesis: 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= (left_open_halfline x0) /\ (dom f)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng a or x in (left_open_halfline x0) /\ (dom f) )
assume x in rng a ; :: thesis: x in (left_open_halfline x0) /\ (dom f)
then consider n being Element of NAT such that
A13: x = a . n by FUNCT_2:113;
a . n in [.(x0 - (r / (n + 1))),x0.] by A11;
then a . n in { g1 where g1 is Real : ( x0 - (r / (n + 1)) <= g1 & g1 <= x0 ) } by RCOMP_1:def 1;
then A14: ex g1 being Real st
( g1 = a . n & x0 - (r / (n + 1)) <= g1 & g1 <= x0 ) ;
a . n <> x0 by A2, A11;
then a . n < x0 by A14, XXREAL_0:1;
then a . n in { g1 where g1 is Real : g1 < x0 } ;
then A15: a . n in left_open_halfline x0 by XXREAL_1:229;
a . n in dom f by A11;
hence x in (left_open_halfline x0) /\ (dom f) by A13, A15, XBOOLE_0:def 4; :: thesis: verum
end;
A16: (left_open_halfline x0) /\ (dom f) c= dom f by XBOOLE_1:17;
A17: for n being Element of NAT holds (f /* a) . n = g2
proof
let n be Element of NAT ; :: thesis: (f /* a) . n = g2
thus (f /* a) . n = f . (a . n) by A12, A16, FUNCT_2:108, XBOOLE_1:1
.= g2 by A11 ; :: thesis: verum
end;
now :: thesis: for n being Nat holds (f /* a) . n = (f /* a) . (n + 1)
let n be Nat; :: thesis: (f /* a) . n = (f /* a) . (n + 1)
n in NAT by ORDINAL1:def 12;
then (f /* a) . n = g2 by A17;
hence (f /* a) . n = (f /* a) . (n + 1) by A17; :: thesis: verum
end;
then A18: lim (f /* a) = (f /* a) . 0 by SEQ_4:26, VALUED_0:25
.= g2 by A17 ;
reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
deffunc H1( Nat) -> set = x0 - (r / ($1 + 1));
consider b being Real_Sequence such that
A19: for n being Nat holds b . n = H1(n) from SEQ_1:sch 1();
A20: now :: thesis: for n being Nat holds
( b . n <= a . n & a . n <= (seq_const x0) . n )
let n be Nat; :: thesis: ( b . n <= a . n & a . n <= (seq_const x0) . n )
A21: n in NAT by ORDINAL1:def 12;
a . n in [.(x0 - (r / (n + 1))),x0.] by A11, A21;
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 <= (seq_const x0) . n ) by A19, SEQ_1:57; :: thesis: verum
end;
A22: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
( b is convergent & lim b = x0 ) by A19, FCONT_3:5;
then ( a is convergent & lim a = x0 ) by A22, A20, SEQ_2:19, SEQ_2:20;
hence contradiction by A1, A2, A12, A18; :: thesis: verum