let a, b, C be Real; :: thesis: for u being PartFunc of REAL,REAL st a < b & ['a,b'] c= dom u & u is continuous & ( for t being Real st t in ].a,b.[ holds
u . t = C ) holds
for t being Real st t in ['a,b'] holds
u . t = C
let u be PartFunc of REAL,REAL; :: thesis: ( a < b & ['a,b'] c= dom u & u is continuous & ( for t being Real st t in ].a,b.[ holds
u . t = C ) implies for t being Real st t in ['a,b'] holds
u . t = C )
assume that
A1: ( a < b & ['a,b'] c= dom u & u is continuous ) and
A2: for t being Real st t in ].a,b.[ holds
u . t = C ; :: thesis: for t being Real st t in ['a,b'] holds
u . t = C
A3: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A4: ].a,b.[ c= ['a,b'] by XXREAL_1:25;
set z = a + ((b - a) / 2);
A5: 0 < b - a by A1, XREAL_1:50;
then (b - a) / 2 < b - a by XREAL_1:216;
then A7: a + ((b - a) / 2) < (b - a) + a by XREAL_1:8;
deffunc H₁( Nat) -> Element of REAL = In ((((b - a) / 2) / ($1 + 1)),REAL);
consider Sn being Function of NAT,REAL such that
A8: for x being Element of NAT holds Sn . x = H₁(x) from FUNCT_2:sch 4();
A9: for n being Nat holds Sn . n = ((b - a) / 2) / (n + 1)

proof

let n be Nat; :: thesis: Sn . n = ((b - a) / 2) / (n + 1)
n in NAT by ORDINAL1:def 12;
hence Sn . n = In ((((b - a) / 2) / (n + 1)),REAL) by A8
.= ((b - a) / 2) / (n + 1) ;
:: thesis: verum

end;

then A10: ( Sn is convergent & lim Sn = 0 ) by SEQ_4:31;
consider Sa being constant Function of NAT,REAL such that
A12: for x being Nat holds Sa . x = a by LmX;
Sa . 0 = a by A12;
then A15: ( Sa is convergent & lim Sa = a ) by SEQ_4:25;
set S0 = Sa + Sn;
A17: lim (Sa + Sn) = a + 0 by A10, A15, SEQ_2:6
.= a ;
a in [.a,b.] by A1;
then A18: u is_continuous_in a by A1, A3;
A19: rng (Sa + Sn) c= ].a,b.[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sa + Sn) or y in ].a,b.[ )
assume y in rng (Sa + Sn) ; :: thesis: y in ].a,b.[
then consider n being object such that
A20: ( n in dom (Sa + Sn) & y = (Sa + Sn) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A20;
A21: y = (Sa . n) + (Sn . n) by A20, SEQ_1:7
.= a + (Sn . n) by A12
.= a + (((b - a) / 2) / (n + 1)) by A9 ;
A22: a + 0 < a + (((b - a) / 2) / (n + 1)) by A5, XREAL_1:8;
1 + 0 <= n + 1 by XREAL_1:7;
then ((b - a) / 2) / (n + 1) <= ((b - a) / 2) / 1 by A5, XREAL_1:118;
then a + (((b - a) / 2) / (n + 1)) <= a + ((b - a) / 2) by XREAL_1:7;
then a + (((b - a) / 2) / (n + 1)) < b by A7, XXREAL_0:2;
hence y in ].a,b.[ by A21, A22; :: thesis: verum

end;

then A23: rng (Sa + Sn) c= dom u by A1, A4;
then A24: ( u /* (Sa + Sn) is convergent & u . a = lim (u /* (Sa + Sn)) ) by A10, A17, A18;
A25: for n being Nat holds (u /* (Sa + Sn)) . n = C

proof

let n be Nat; :: thesis: (u /* (Sa + Sn)) . n = C
A26: n in NAT by ORDINAL1:def 12;
then A27: (u /* (Sa + Sn)) . n = u . ((Sa + Sn) . n) by A23, FUNCT_2:108;
(Sa + Sn) . n in rng (Sa + Sn) by A26, FUNCT_2:112;
hence (u /* (Sa + Sn)) . n = C by A2, A19, A27; :: thesis: verum

end;

for x, y being object st x in dom (u /* (Sa + Sn)) & y in dom (u /* (Sa + Sn)) holds
(u /* (Sa + Sn)) . x = (u /* (Sa + Sn)) . y

proof

let x, y be object ; :: thesis: ( x in dom (u /* (Sa + Sn)) & y in dom (u /* (Sa + Sn)) implies (u /* (Sa + Sn)) . x = (u /* (Sa + Sn)) . y )
assume ( x in dom (u /* (Sa + Sn)) & y in dom (u /* (Sa + Sn)) ) ; :: thesis: (u /* (Sa + Sn)) . x = (u /* (Sa + Sn)) . y
then reconsider x0 = x, y0 = y as Element of NAT ;
thus (u /* (Sa + Sn)) . x = (u /* (Sa + Sn)) . x0
.= C by A25
.= (u /* (Sa + Sn)) . y0 by A25
.= (u /* (Sa + Sn)) . y ; :: thesis: verum

end;

then A28: u /* (Sa + Sn) is constant by FUNCT_1:def 10;
A29: (u /* (Sa + Sn)) . 0 = C by A25;
consider Sb being constant Function of NAT,REAL such that
A30: for x being Nat holds Sb . x = b by LmX;
A33: Sb . 0 = b by A30;
set S1 = Sb - Sn;
( Sb - Sn is convergent & lim (Sb - Sn) = (lim Sb) - (lim Sn) ) by A10, SEQ_2:12;
then A35: lim (Sb - Sn) = b by A10, A33, SEQ_4:25;
b in [.a,b.] by A1;
then A36: u is_continuous_in b by A1, A3;
A37: rng (Sb - Sn) c= ].a,b.[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sb - Sn) or y in ].a,b.[ )
assume y in rng (Sb - Sn) ; :: thesis: y in ].a,b.[
then consider n being object such that
A38: ( n in dom (Sb - Sn) & y = (Sb - Sn) . n ) by FUNCT_1:def 3;
reconsider n = n as Nat by A38;
A39: y = (Sb . n) + ((- Sn) . n) by A38, SEQ_1:7
.= (Sb . n) - (Sn . n) by SEQ_1:10
.= b - (Sn . n) by A30
.= b - (((b - a) / 2) / (n + 1)) by A9 ;
A40: b - (((b - a) / 2) / (n + 1)) < b - 0 by A5, XREAL_1:15;
1 + 0 <= n + 1 by XREAL_1:7;
then ((b - a) / 2) / (n + 1) <= ((b - a) / 2) / 1 by A5, XREAL_1:118;
then A41: b - ((b - a) / 2) <= b - (((b - a) / 2) / (n + 1)) by XREAL_1:13;
a + 0 < a + ((b - a) / 2) by A5, XREAL_1:8;
then a < b - (((b - a) / 2) / (n + 1)) by A41, XXREAL_0:2;
hence y in ].a,b.[ by A39, A40; :: thesis: verum

end;

then A42: rng (Sb - Sn) c= dom u by A1, A4;
then A43: ( u /* (Sb - Sn) is convergent & u . b = lim (u /* (Sb - Sn)) ) by A10, A35, A36;
A44: for n being Nat holds (u /* (Sb - Sn)) . n = C

proof

let n be Nat; :: thesis: (u /* (Sb - Sn)) . n = C
A45: n in NAT by ORDINAL1:def 12;
then A46: (u /* (Sb - Sn)) . n = u . ((Sb - Sn) . n) by A42, FUNCT_2:108;
(Sb - Sn) . n in ].a,b.[ by A37, A45, FUNCT_2:112;
hence (u /* (Sb - Sn)) . n = C by A2, A46; :: thesis: verum

end;

for x, y being object st x in dom (u /* (Sb - Sn)) & y in dom (u /* (Sb - Sn)) holds
(u /* (Sb - Sn)) . x = (u /* (Sb - Sn)) . y

proof

let x, y be object ; :: thesis: ( x in dom (u /* (Sb - Sn)) & y in dom (u /* (Sb - Sn)) implies (u /* (Sb - Sn)) . x = (u /* (Sb - Sn)) . y )
assume ( x in dom (u /* (Sb - Sn)) & y in dom (u /* (Sb - Sn)) ) ; :: thesis: (u /* (Sb - Sn)) . x = (u /* (Sb - Sn)) . y
then reconsider x0 = x, y0 = y as Element of NAT ;
thus (u /* (Sb - Sn)) . x = (u /* (Sb - Sn)) . x0
.= C by A44
.= (u /* (Sb - Sn)) . y0 by A44
.= (u /* (Sb - Sn)) . y ; :: thesis: verum

end;

then A47: u /* (Sb - Sn) is constant by FUNCT_1:def 10;
A48: (u /* (Sb - Sn)) . 0 = C by A44;
thus for t being Real st t in ['a,b'] holds
u . t = C :: thesis: verum

proof

let t be Real; :: thesis: ( t in ['a,b'] implies u . t = C )
assume t in ['a,b'] ; :: thesis: u . t = C
then ex r being Real st
( t = r & a <= r & r <= b ) by A3;

per cases then ( t = a or ( a < t & t < b ) or t = b ) by XXREAL_0:1;

suppose t = a ; :: thesis: u . t = C

hence u . t = C by A24, A28, A29, SEQ_4:25; :: thesis: verum

end;

suppose ( a < t & t < b ) ; :: thesis: u . t = C

then t in ].a,b.[ ;
hence u . t = C by A2; :: thesis: verum

end;

suppose t = b ; :: thesis: u . t = C

hence u . t = C by A43, A47, A48, SEQ_4:25; :: thesis: verum

end;

end;

end;