let X be RealBanachSpace; :: thesis:
let a, b be Real; :: thesis:
let f be continuous PartFunc of REAL, the carrier of X; :: thesis:
assume A1: ( [.a,b.] = dom f & f | ].a,b.[ is constant ) ; :: thesis:
A2: ].a,b.[ c= [.a,b.] by XXREAL_1:25;

per cases ;

suppose X0: a >= b ; :: thesis:

hereby :: thesis:

let x be Real; :: thesis:
assume x in [.a,b.] ; :: thesis:
then ( a <= x & x <= b ) by XXREAL_1:1;
then ( a <= x & x <= a ) by X0, XXREAL_0:2;
hence f /. x = f /. a by XXREAL_0:1; :: thesis:

end;

suppose A0: a < b ; :: thesis:

reconsider d = (b - a) / 2 as Real ;
A3: 0 < b - a by A0, XREAL_1:50;
then A4: 0 < d by XREAL_1:215;
a + ((b - a) / 2) = (a + b) / 2 ;
then A5: ( a < a + d & a + d < b ) by A0, XREAL_1:226;
then a + d in ].a,b.[ ;
then f . (a + d) in rng f by A2, A1, FUNCT_1:3;
then reconsider f0 = f . (a + d) as Point of X ;
dom (f | ].a,b.[) = (dom f) /\ ].a,b.[ by RELAT_1:61;
then A6: dom (f | ].a,b.[) = ].a,b.[ by A1, XXREAL_1:25, XBOOLE_1:28;

A7: now :: thesis:

let x be Real; :: thesis:
assume A8: x in ].a,b.[ ; :: thesis:
A9: a + d in dom (f | ].a,b.[) by A5, A6;
thus f /. x = f . x by A8, A2, A1, PARTFUN1:def 6
.= (f | ].a,b.[) . x by A6, A8, FUNCT_1:47
.= (f | ].a,b.[) . (a + d) by A1, A6, A8, A9, FUNCT_1:def 10
.= f0 by A9, FUNCT_1:47 ; :: thesis:

end;

( a in dom f & b in dom f ) by A1, A0;
then A14: ( f is_continuous_in a & f is_continuous_in b ) by NFCONT_3:def 2;
deffunc H₁( Nat) -> set = a + (d / ($1 + 1));
A12: for x being Element of NAT holds H₁(x) is Element of REAL by XREAL_0:def 1;
consider s1 being Real_Sequence such that
A13: for x being Element of NAT holds s1 . x = H₁(x) from FUNCT_2:sch 9(A12);

A15: now :: thesis:

let y be object ; :: thesis:
assume y in rng s1 ; :: thesis:
then consider x being object such that
A16: ( x in dom s1 & y = s1 . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A16;
A17: y = a + (d / (x + 1)) by A13, A16;
0 < d / (x + 1) by A4, XREAL_1:139;
then A20: a + 0 < a + (d / (x + 1)) by XREAL_1:8;
1 + 0 <= 1 + x by XREAL_1:7;
then d / (x + 1) <= d / 1 by XREAL_1:118, A3;
then a + (d / (x + 1)) <= a + d by XREAL_1:7;
then a + (d / (x + 1)) < b by A5, XXREAL_0:2;
hence y in ].a,b.[ by A17, A20; :: thesis:

end;

then A21: ( rng s1 c= ].a,b.[ & rng s1 c= dom f ) by A2, A1;

A23: now :: thesis:

let p be Real; :: thesis:
assume A24: 0 < p ; :: thesis:
consider n being Nat such that
A25: d / p < n by SEQ_4:3;
n + 0 < n + 1 by XREAL_1:8;
then d / p < n + 1 by XXREAL_0:2, A25;
then (d / p) * p < (n + 1) * p by A24, XREAL_1:68;
then d < (n + 1) * p by A24, XCMPLX_1:87;
then d / (n + 1) < p by XREAL_1:83;
then A29: |.(d / (n + 1)).| < p by A3, ABSVALUE:def 1;
A28: |.(d / (n + 1)).| = d / (n + 1) by A3, ABSVALUE:def 1;
take n = n; :: thesis:
thus for m being Nat st n <= m holds
|.((s1 . m) - a).| < p :: thesis:

proof

let m be Nat; :: thesis:
K: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
then n + 1 <= m + 1 by XREAL_1:7;
then d / (m + 1) <= d / (n + 1) by A3, XREAL_1:118;
then A31: |.(d / (m + 1)).| <= |.(d / (n + 1)).| by A28, A3, ABSVALUE:def 1;
|.((s1 . m) - a).| = |.((a + (d / (m + 1))) - a).| by A13, K;
hence |.((s1 . m) - a).| < p by A31, A29, XXREAL_0:2; :: thesis:

end;

then A32: s1 is convergent by SEQ_2:def 6;
then lim s1 = a by A23, SEQ_2:def 7;
then A34: ( f /* s1 is convergent & f /. a = lim (f /* s1) ) by A14, A21, A32;
A35: for i being Nat holds (f /* s1) . i = f0

proof

let i be Nat; :: thesis:
S: i in NAT by ORDINAL1:def 12;
A36: s1 . i in rng s1 by FUNCT_2:4, ORDINAL1:def 12;
thus (f /* s1) . i = f /. (s1 . i) by A21, FUNCT_2:109, S
.= f0 by A7, A36, A15 ; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume A37: 0 < r ; :: thesis:
reconsider m = the Element of NAT as Nat ;
take m = m; :: thesis:
thus for k being Nat st m <= k holds
||.(((f /* s1) . k) - f0).|| < r :: thesis:

proof

let k be Nat; :: thesis:
assume m <= k ; :: thesis:
||.(((f /* s1) . k) - f0).|| = ||.(f0 - f0).|| by A35
.= ||.(0. X).|| by RLVECT_1:15 ;
hence ||.(((f /* s1) . k) - f0).|| < r by A37; :: thesis:

end;

then A38: f /. a = f0 by A34, NORMSP_1:def 7;
deffunc H₂( Nat) -> set = b - (d / ($1 + 1));
A39: for x being Element of NAT holds H₂(x) is Element of REAL by XREAL_0:def 1;
consider s2 being Real_Sequence such that
A40: for x being Element of NAT holds s2 . x = H₂(x) from FUNCT_2:sch 9(A39);

A42: now :: thesis:

let y be object ; :: thesis:
assume y in rng s2 ; :: thesis:
then consider x being object such that
A43: ( x in dom s2 & y = s2 . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A43;
A44: y = b - (d / (x + 1)) by A40, A43;
0 < d / (x + 1) by A4, XREAL_1:139;
then A47: b - (d / (x + 1)) < b - 0 by XREAL_1:15;
1 + 0 <= 1 + x by XREAL_1:7;
then d / (x + 1) <= d / 1 by XREAL_1:118, A3;
then b - d <= b - (d / (x + 1)) by XREAL_1:13;
then a < b - (d / (x + 1)) by A5, XXREAL_0:2;
hence y in ].a,b.[ by A44, A47; :: thesis:

end;

then A48: ( rng s2 c= ].a,b.[ & rng s2 c= dom f ) by A2, A1;

A50: now :: thesis:

let p be Real; :: thesis:
assume A51: 0 < p ; :: thesis:
consider n being Nat such that
A52: d / p < n by SEQ_4:3;
n + 0 < n + 1 by XREAL_1:8;
then d / p < n + 1 by XXREAL_0:2, A52;
then (d / p) * p < (n + 1) * p by A51, XREAL_1:68;
then d < (n + 1) * p by A51, XCMPLX_1:87;
then A54: d / (n + 1) < p by XREAL_1:83;
take n = n; :: thesis:
thus for m being Nat st n <= m holds
|.((s2 . m) - b).| < p :: thesis:

proof

let m be Nat; :: thesis:
K: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
then n + 1 <= m + 1 by XREAL_1:7;
then d / (m + 1) <= d / (n + 1) by A3, XREAL_1:118;
then A57: |.(d / (m + 1)).| <= d / (n + 1) by A3, ABSVALUE:def 1;
|.((s2 . m) - b).| = |.((b - (d / (m + 1))) - b).| by A40, K
.= |.(d / (m + 1)).| by COMPLEX1:52 ;
hence |.((s2 . m) - b).| < p by A57, XXREAL_0:2, A54; :: thesis:

end;

then A58: s2 is convergent by SEQ_2:def 6;
then lim s2 = b by A50, SEQ_2:def 7;
then A60: ( f /* s2 is convergent & f /. b = lim (f /* s2) ) by A14, A48, A58;
A61: for i being Element of NAT holds (f /* s2) . i = f0

proof

let i be Element of NAT ; :: thesis:
s2 . i in rng s2 by FUNCT_2:4;
then f /. (s2 . i) = f0 by A7, A42;
hence (f /* s2) . i = f0 by A48, FUNCT_2:109; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume A63: 0 < r ; :: thesis:
reconsider m = the Element of NAT as Nat ;
take m = m; :: thesis:
thus for k being Nat st m <= k holds
||.(((f /* s2) . k) - f0).|| < r :: thesis:

proof

let k be Nat; :: thesis:
assume m <= k ; :: thesis:
k in NAT by ORDINAL1:def 12;
then ||.(((f /* s2) . k) - f0).|| = ||.(f0 - f0).|| by A61
.= ||.(0. X).|| by RLVECT_1:15
.= 0 ;
hence ||.(((f /* s2) . k) - f0).|| < r by A63; :: thesis:

end;

then A64: f /. b = f0 by A60, NORMSP_1:def 7;
let x be Real; :: thesis:
assume x in [.a,b.] ; :: thesis:
then A65: ex r being Real st
( x = r & a <= r & r <= b ) ;

per cases ;

suppose x in ].a,b.[ ; :: thesis:

hence f /. x = f /. a by A38, A7; :: thesis:

end;

suppose not x in ].a,b.[ ; :: thesis:

then ( x <= a or b <= x ) ;
hence f /. x = f /. a by A38, A64, A65, XXREAL_0:1; :: thesis:

end;