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_{1}[ 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 Element of REAL st S_{1}[n,g]

A11: for n being Element of NAT holds S_{1}[n,a . n]
from FUNCT_2:sch 3(A6);

A12: rng a c= (right_open_halfline x0) /\ (dom f)

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

.= g2 by A17 ;

deffunc H_{1}( 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 = H_{1}(n)
from SEQ_1:sch 1();

then ( a is convergent & lim a = x0 ) by A19, A21, SEQ_2:19, SEQ_2:20;

hence contradiction by A1, A2, A12, A18; :: thesis: verum

( 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

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 Element of REAL st S

proof

consider a being Real_Sequence such that
let n be Element of NAT ; :: thesis: ex g being Element of REAL st S_{1}[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 ; :: thesis: ( g is set & g is Element of REAL & S_{1}[n,g] )

thus ( g is set & g is Element of REAL & S_{1}[n,g] )
by A9, A10; :: thesis: verum

end;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 ; :: thesis: ( g is set & g is Element of REAL & S

thus ( g is set & g is Element of REAL & S

A11: for n being Element of NAT holds S

A12: rng a c= (right_open_halfline x0) /\ (dom f)

proof

A16:
(right_open_halfline x0) /\ (dom f) c= dom f
by XBOOLE_1:17;
let x be object ; :: 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

A13: x = a . n by FUNCT_2:113;

a . n in [.x0,(x0 + (r / (n + 1))).] by A11;

then a . n in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) } by RCOMP_1:def 1;

then A14: ex g1 being Real st

( g1 = a . n & x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) ;

x0 <> a . n by A2, A11;

then x0 < a . n by A14, XXREAL_0:1;

then a . n in { g1 where g1 is Real : x0 < g1 } ;

then A15: a . n in right_open_halfline x0 by XXREAL_1:230;

a . n in dom f by A11;

hence x in (right_open_halfline x0) /\ (dom f) by A13, A15, XBOOLE_0:def 4; :: thesis: verum

end;assume x in rng a ; :: thesis: x in (right_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,(x0 + (r / (n + 1))).] by A11;

then a . n in { g1 where g1 is Real : ( x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) } by RCOMP_1:def 1;

then A14: ex g1 being Real st

( g1 = a . n & x0 <= g1 & g1 <= x0 + (r / (n + 1)) ) ;

x0 <> a . n by A2, A11;

then x0 < a . n by A14, XXREAL_0:1;

then a . n in { g1 where g1 is Real : x0 < g1 } ;

then A15: a . n in right_open_halfline x0 by XXREAL_1:230;

a . n in dom f by A11;

hence x in (right_open_halfline x0) /\ (dom f) by A13, A15, XBOOLE_0:def 4; :: thesis: verum

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 g2 = f . (a . n) by A11

.= (f /* a) . n by A12, A16, FUNCT_2:108, XBOOLE_1:1 ; :: thesis: verum

end;thus g2 = f . (a . n) by A11

.= (f /* a) . n by A12, A16, FUNCT_2:108, XBOOLE_1:1 ; :: thesis: verum

now :: thesis: for n being Nat holds (f /* a) . n = (f /* a) . (n + 1)

then A18: lim (f /* a) =
(f /* a) . 0
by SEQ_4:26, VALUED_0:25
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;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

.= g2 by A17 ;

deffunc H

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 = H

A21: now :: thesis: for n being Nat holds

( (seq_const x0) . n <= a . n & a . n <= d . n )

( d is convergent & lim d = x0 )
by A20, FCONT_3:6;( (seq_const x0) . n <= a . n & a . n <= d . n )

let n be Nat; :: thesis: ( (seq_const x0) . n <= a . n & a . n <= d . n )

A22: n in NAT by ORDINAL1:def 12;

a . n in [.x0,(x0 + (r / (n + 1))).] by A11, A22;

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 ( (seq_const x0) . n <= a . n & a . n <= d . n ) by A20, SEQ_1:57; :: thesis: verum

end;A22: n in NAT by ORDINAL1:def 12;

a . n in [.x0,(x0 + (r / (n + 1))).] by A11, A22;

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 ( (seq_const x0) . n <= a . n & a . n <= d . n ) by A20, SEQ_1:57; :: thesis: verum

then ( a is convergent & lim a = x0 ) by A19, A21, SEQ_2:19, SEQ_2:20;

hence contradiction by A1, A2, A12, A18; :: thesis: verum