let n be non zero Element of NAT ; :: thesis:
let a, b be Real; :: thesis:
let f be continuous PartFunc of REAL,(REAL-NS n); :: thesis:
assume A1: ( a < b & [.a,b.] = dom f & f | ].a,b.[ is constant ) ; :: thesis:
A2: ].a,b.[ c= [.a,b.] by XXREAL_1:25;
reconsider d = (b - a) / 2 as Real ;
A3: 0 < b - a by A1, 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 A1, 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 (REAL-NS n) ;
A6: dom (f | ].a,b.[) = (dom f) /\ ].a,b.[ by RELAT_1:61
.= ].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;

A10: a in dom f by A1;
A11: b in dom f by A1;
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);
A14: f is_continuous_in a by A10, NFCONT_3:def 2;

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;
A18: 0 < d / (x + 1) by A4, XREAL_1:139;
1 + 0 <= 1 + x by XREAL_1:7;
then A19: d / (x + 1) <= d / 1 by XREAL_1:118, A3;
A20: a + 0 < a + (d / (x + 1)) by A18, XREAL_1:8;
a + (d / (x + 1)) <= a + d by A19, 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.[ by TARSKI:def 3;
then A22: rng s1 c= dom f by A2, A1, XBOOLE_1:1;

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 A26: d < (n + 1) * p by A24, XCMPLX_1:87;
A27: d / (n + 1) < p by A26, XREAL_1:83;
A28: |.(d / (n + 1)).| = d / (n + 1) by A3, ABSVALUE:def 1;
A29: |.(d / (n + 1)).| < p by A27, 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:
A30: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
then A31: n + 1 <= m + 1 by XREAL_1:7;
d / (m + 1) <= d / (n + 1) by A3, A31, XREAL_1:118;
then A32: |.(d / (m + 1)).| <= |.(d / (n + 1)).| by A28, A3, ABSVALUE:def 1;
|.((s1 . m) - a).| = |.((a + (d / (m + 1))) - a).| by A13, A30
.= |.(d / (m + 1)).| ;
hence |.((s1 . m) - a).| < p by A32, A29, XXREAL_0:2; :: thesis:

end;

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

proof

let i be Nat; :: thesis:
A37: i in NAT by ORDINAL1:def 12;
then A38: s1 . i in rng s1 by FUNCT_2:4;
thus (f /* s1) . i = f /. (s1 . i) by A21, FUNCT_2:109, XBOOLE_1:1, A1, A2, A37
.= f0 by A7, A38, A15 ; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume A39: 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 A36
.= ||.(0. (REAL-NS n)).|| by RLVECT_1:15
.= 0 ;
hence ||.(((f /* s1) . k) - f0).|| < r by A39; :: thesis:

end;

then lim (f /* s1) = f0 by A35, NORMSP_1:def 7;
then A40: f . a = f0 by A35, A10, PARTFUN1:def 6;
deffunc H₂( Nat) -> set = b - (d / ($1 + 1));
A41: 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
A42: for x being Element of NAT holds s2 . x = H₂(x) from FUNCT_2:sch 9(A41);
A43: f is_continuous_in b by A11, NFCONT_3:def 2;

A44: now :: thesis:

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

end;

then A50: rng s2 c= ].a,b.[ by TARSKI:def 3;
then A51: rng s2 c= dom f by A2, A1, XBOOLE_1:1;

A52: now :: thesis:

let p be Real; :: thesis:
assume A53: 0 < p ; :: thesis:
consider n being Nat such that
A54: d / p < n by SEQ_4:3;
n + 0 < n + 1 by XREAL_1:8;
then d / p < n + 1 by XXREAL_0:2, A54;
then (d / p) * p < (n + 1) * p by A53, XREAL_1:68;
then A55: d < (n + 1) * p by A53, XCMPLX_1:87;
A56: d / (n + 1) < p by A55, 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:
A57: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis:
then A58: n + 1 <= m + 1 by XREAL_1:7;
A59: d / (m + 1) <= d / (n + 1) by A3, A58, XREAL_1:118;
A60: |.(d / (m + 1)).| = d / (m + 1) by A3, ABSVALUE:def 1;
|.((s2 . m) - b).| = |.((b - (d / (m + 1))) - b).| by A42, A57
.= |.(- (d / (m + 1))).|
.= |.(d / (m + 1)).| by COMPLEX1:52 ;
hence |.((s2 . m) - b).| < p by A60, XXREAL_0:2, A59, A56; :: thesis:

end;

then A61: s2 is convergent by SEQ_2:def 6;
then A62: lim s2 = b by A52, SEQ_2:def 7;
A63: ( f /* s2 is convergent & f /. b = lim (f /* s2) ) by A43, A51, A61, A62, NFCONT_3:def 1;
A64: for i being Element of NAT holds (f /* s2) . i = f0

proof

let i be Element of NAT ; :: thesis:
A65: s2 . i in rng s2 by FUNCT_2:4;
thus (f /* s2) . i = f /. (s2 . i) by A2, A1, XBOOLE_1:1, A50, FUNCT_2:109
.= f0 by A7, A65, A44 ; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume A66: 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 A64
.= ||.(0. (REAL-NS n)).|| by RLVECT_1:15
.= 0 ;
hence ||.(((f /* s2) . k) - f0).|| < r by A66; :: thesis:

end;

then lim (f /* s2) = f0 by A63, NORMSP_1:def 7;
then A67: f . b = f0 by A63, A11, PARTFUN1:def 6;
let x be Real; :: thesis:
assume x in [.a,b.] ; :: thesis:
then A68: ex r being Real st
( x = r & a <= r & r <= b ) ;

per cases ;

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

hence f . x = f /. x by A1, A2, PARTFUN1:def 6
.= f . a by A40, A69, A7 ;
:: thesis:

end;

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

then ( x <= a or b <= x ) ;
hence f . x = f . a by A40, A67, A68, XXREAL_0:1; :: thesis:

end;