let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f | ['a,b'] is continuous holds
ex I being Real_Sequence st
( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) )
let a, b be Real; :: thesis: ( a < b & ['a,b'] c= dom f & f | ['a,b'] is continuous implies ex I being Real_Sequence st
( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) ) )
assume that
A1: ( a < b & ['a,b'] c= dom f ) and
A2: f | ['a,b'] is continuous ; :: thesis: ex I being Real_Sequence st
( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) )
A3: ( f | ['a,b'] is bounded & f is_integrable_on ['a,b'] ) by A1, A2, INTEGRA5:10, INTEGRA5:11;
deffunc H₁( Nat) -> Element of REAL = In ((integral (f,(a + (1 / ($1 + 1))),(b - (1 / ($1 + 1))))),REAL);
consider I being Function of NAT,REAL such that
A4: for x being Element of NAT holds I . x = H₁(x) from FUNCT_2:sch 4();
take I ; :: thesis: ( ( for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) ) & I is convergent & lim I = integral (f,a,b) )
thus A5: for n being Nat holds I . n = integral (f,(a + (1 / (n + 1))),(b - (1 / (n + 1)))) :: thesis: ( I is convergent & lim I = integral (f,a,b) )

proof

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

end;

A6: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
set X = ['a,b'];
dom (abs f) = dom f by VALUED_1:def 11;
then A8: dom ((abs f) | ['a,b']) = ['a,b'] by A1, RELAT_1:62;
A9: ((abs f) | ['a,b']) | (dom ((abs f) | ['a,b'])) is continuous by A1, A2, FCONT_1:21;
then consider t1, t2 being Real such that
A10: ( t1 in dom ((abs f) | ['a,b']) & t2 in dom ((abs f) | ['a,b']) & ((abs f) | ['a,b']) . t1 = upper_bound (rng ((abs f) | ['a,b'])) & ((abs f) | ['a,b']) . t2 = lower_bound (rng ((abs f) | ['a,b'])) ) by A8, FCONT_1:30;
set K = ((abs f) | ['a,b']) . t1;
A11: rng ((abs f) | ['a,b']) is real-bounded by A8, A9, FCONT_1:28, RCOMP_1:10;
A12: for t being Real st t in ['a,b'] holds
|.(f . t).| <= ((abs f) | ['a,b']) . t1

proof

let t be Real; :: thesis: ( t in ['a,b'] implies |.(f . t).| <= ((abs f) | ['a,b']) . t1 )
assume A13: t in ['a,b'] ; :: thesis: |.(f . t).| <= ((abs f) | ['a,b']) . t1
then ((abs f) | ['a,b']) . t in rng ((abs f) | ['a,b']) by A8, FUNCT_1:3;
then ((abs f) | ['a,b']) . t <= ((abs f) | ['a,b']) . t1 by A10, A11, SEQ_4:def 1;
then (abs f) . t <= ((abs f) | ['a,b']) . t1 by A13, FUNCT_1:49;
hence |.(f . t).| <= ((abs f) | ['a,b']) . t1 by VALUED_1:18; :: thesis: verum

end;

set L = integral (f,a,b);
A15: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (integral (f,a,b))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (integral (f,a,b))).| < p )
assume B15: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((I . m) - (integral (f,a,b))).| < p
then A16: ( 0 < p / 2 & p / 2 < p ) by XREAL_1:216;
set e = p / 2;
consider N1 being Nat such that
A17: 2 / (b - a) < N1 by SEQ_4:3;
N1 + 0 < N1 + 1 by XREAL_1:8;
then A18: 2 / (b - a) < N1 + 1 by A17, XXREAL_0:2;
consider N2 being Nat such that
A19: (2 * ((((abs f) | ['a,b']) . t1) + 1)) / (p / 2) < N2 by SEQ_4:3;
N2 + 0 < N2 + 1 by XREAL_1:8;
then A20: (2 * ((((abs f) | ['a,b']) . t1) + 1)) / (p / 2) < N2 + 1 by A19, XXREAL_0:2;
reconsider n = max (N1,N2) as Nat by XXREAL_0:16;
take n ; :: thesis: for m being Nat st n <= m holds
|.((I . m) - (integral (f,a,b))).| < p
let m be Nat; :: thesis: ( n <= m implies |.((I . m) - (integral (f,a,b))).| < p )
assume A21: n <= m ; :: thesis: |.((I . m) - (integral (f,a,b))).| < p
N1 <= n by XXREAL_0:25;
then N1 <= m by A21, XXREAL_0:2;
then N1 + 1 <= m + 1 by XREAL_1:7;
then A22: 2 / (b - a) <= m + 1 by A18, XXREAL_0:2;
A23: 0 < b - a by A1, XREAL_1:50;
then (2 / (b - a)) * (b - a) <= (m + 1) * (b - a) by A22, XREAL_1:64;
then 2 <= (m + 1) * (b - a) by A23, XCMPLX_1:87;
then A24: 2 / 2 <= ((m + 1) * (b - a)) / 2 by XREAL_1:72;
(((m + 1) * (b - a)) / 2) / (m + 1) = ((m + 1) / (m + 1)) * ((b - a) / 2)
.= 1 * ((b - a) / 2) by XCMPLX_1:60 ;
then A25: 1 / (m + 1) <= (b - a) / 2 by A24, XREAL_1:72;
N2 <= n by XXREAL_0:25;
then N2 <= m by A21, XXREAL_0:2;
then N2 + 1 <= m + 1 by XREAL_1:7;
then (2 * ((((abs f) | ['a,b']) . t1) + 1)) / (p / 2) <= m + 1 by A20, XXREAL_0:2;
then ((2 * ((((abs f) | ['a,b']) . t1) + 1)) / (p / 2)) / 2 <= (m + 1) / 2 by XREAL_1:72;
then (((((abs f) | ['a,b']) . t1) + 1) / (p / 2)) * (p / 2) <= ((m + 1) / 2) * (p / 2) by B15, XREAL_1:64;
then A26: (((abs f) | ['a,b']) . t1) + 1 <= ((p / 2) * (m + 1)) / 2 by B15, XCMPLX_1:87;
(((p / 2) * (m + 1)) / 2) / (m + 1) = ((m + 1) / (m + 1)) * ((p / 2) / 2)
.= 1 * ((p / 2) / 2) by XCMPLX_1:60 ;
then A27: ((((abs f) | ['a,b']) . t1) + 1) / (m + 1) <= (p / 2) / 2 by A26, XREAL_1:72;
(1 / (m + 1)) + (1 / (m + 1)) <= ((b - a) / 2) + ((b - a) / 2) by A25, XREAL_1:7;
then ((1 / (m + 1)) + (1 / (m + 1))) + a <= (b - a) + a by XREAL_1:7;
then A28: ((a + (1 / (m + 1))) + (1 / (m + 1))) - (1 / (m + 1)) <= b - (1 / (m + 1)) by XREAL_1:13;
A29: a + 0 <= a + (1 / (m + 1)) by XREAL_1:7;
A30: b - (1 / (m + 1)) <= b - 0 by XREAL_1:13;
then a + (1 / (m + 1)) <= b by A28, XXREAL_0:2;
then A31: a + (1 / (m + 1)) in ['a,b'] by A6, A29;
then A32: ( f is_integrable_on ['a,(a + (1 / (m + 1)))'] & f is_integrable_on ['a,(a + (1 / (m + 1)))'] & integral (f,a,b) = (integral (f,a,(a + (1 / (m + 1))))) + (integral (f,(a + (1 / (m + 1))),b)) ) by A1, A3, INTEGRA6:17;
A33: a + (1 / (m + 1)) <= b by A28, A30, XXREAL_0:2;
A34: ['(a + (1 / (m + 1))),b'] = [.(a + (1 / (m + 1))),b.] by A28, A30, INTEGRA5:def 3, XXREAL_0:2;

B34: now :: thesis: for t being object st t in [.(a + (1 / (m + 1))),b.] holds
t in [.a,b.]

let t be object ; :: thesis: ( t in [.(a + (1 / (m + 1))),b.] implies t in [.a,b.] )
assume A35: t in [.(a + (1 / (m + 1))),b.] ; :: thesis: t in [.a,b.]
then reconsider x = t as Real ;
A36: ( a + (1 / (m + 1)) <= x & x <= b ) by A35, XXREAL_1:1;
then a <= x by A29, XXREAL_0:2;
hence t in [.a,b.] by A36; :: thesis: verum

end;

then A37: [.(a + (1 / (m + 1))),b.] c= [.a,b.] ;
(f | ['a,b']) | ['(a + (1 / (m + 1))),b'] is continuous by A2;
then A38: f | ['(a + (1 / (m + 1))),b'] is continuous by A6, A34, A37, RELAT_1:74;
A39: ['(a + (1 / (m + 1))),b'] c= dom f by A1, A6, A34, B34;
then A40: ( f | ['(a + (1 / (m + 1))),b'] is bounded & f is_integrable_on ['(a + (1 / (m + 1))),b'] ) by A38, INTEGRA5:10, INTEGRA5:11;
b - (1 / (m + 1)) in ['(a + (1 / (m + 1))),b'] by A28, A30, A34;
then A41: integral (f,a,b) = (integral (f,a,(a + (1 / (m + 1))))) + ((integral (f,(a + (1 / (m + 1))),(b - (1 / (m + 1))))) + (integral (f,(b - (1 / (m + 1))),b))) by A32, A33, A39, A40, INTEGRA6:17;
A42: integral (f,(a + (1 / (m + 1))),(b - (1 / (m + 1)))) = I . m by A5;
|.((I . m) - (integral (f,a,b))).| = |.((integral (f,a,b)) - (I . m)).| by COMPLEX1:60
.= |.((integral (f,a,(a + (1 / (m + 1))))) + (integral (f,(b - (1 / (m + 1))),b))).| by A41, A42 ;
then A43: |.((I . m) - (integral (f,a,b))).| <= |.(integral (f,a,(a + (1 / (m + 1))))).| + |.(integral (f,(b - (1 / (m + 1))),b)).| by COMPLEX1:56;
A44: a in ['a,b'] by A1, A6;
for x being Real st x in ['a,(a + (1 / (m + 1)))'] holds
|.(f . x).| <= ((abs f) | ['a,b']) . t1

proof

let x be Real; :: thesis: ( x in ['a,(a + (1 / (m + 1)))'] implies |.(f . x).| <= ((abs f) | ['a,b']) . t1 )
assume x in ['a,(a + (1 / (m + 1)))'] ; :: thesis: |.(f . x).| <= ((abs f) | ['a,b']) . t1
then x in [.a,(a + (1 / (m + 1))).] by A29, INTEGRA5:def 3;
then A45: ( a <= x & x <= a + (1 / (m + 1)) ) by XXREAL_1:1;
a + (1 / (m + 1)) <= b by A28, A30, XXREAL_0:2;
then ( a <= x & x <= b ) by A45, XXREAL_0:2;
then x in ['a,b'] by A6;
hence |.(f . x).| <= ((abs f) | ['a,b']) . t1 by A12; :: thesis: verum

end;

then A46: |.(integral (f,a,(a + (1 / (m + 1))))).| <= (((abs f) | ['a,b']) . t1) * ((a + (1 / (m + 1))) - a) by A1, A3, A29, A31, A44, INTEGRA6:23;
a <= b - (1 / (m + 1)) by A28, A29, XXREAL_0:2;
then A47: b - (1 / (m + 1)) in ['a,b'] by A6, A30;
A48: b in ['a,b'] by A1, A6;
for x being Real st x in ['(b - (1 / (m + 1))),b'] holds
|.(f . x).| <= ((abs f) | ['a,b']) . t1

proof

let x be Real; :: thesis: ( x in ['(b - (1 / (m + 1))),b'] implies |.(f . x).| <= ((abs f) | ['a,b']) . t1 )
assume x in ['(b - (1 / (m + 1))),b'] ; :: thesis: |.(f . x).| <= ((abs f) | ['a,b']) . t1
then x in [.(b - (1 / (m + 1))),b.] by A30, INTEGRA5:def 3;
then A49: ( b - (1 / (m + 1)) <= x & x <= b ) by XXREAL_1:1;
a <= b - (1 / (m + 1)) by A28, A29, XXREAL_0:2;
then ( a <= x & x <= b ) by A49, XXREAL_0:2;
then x in ['a,b'] by A6;
hence |.(f . x).| <= ((abs f) | ['a,b']) . t1 by A12; :: thesis: verum

end;

then A50: |.(integral (f,(b - (1 / (m + 1))),b)).| <= (((abs f) | ['a,b']) . t1) * (b - (b - (1 / (m + 1)))) by A1, A3, A30, A47, A48, INTEGRA6:23;
(((abs f) | ['a,b']) . t1) + 0 <= (((abs f) | ['a,b']) . t1) + 1 by XREAL_1:7;
then (((abs f) | ['a,b']) . t1) * (1 / (m + 1)) <= ((((abs f) | ['a,b']) . t1) + 1) * (1 / (m + 1)) by XREAL_1:64;
then A51: (((abs f) | ['a,b']) . t1) * (1 / (m + 1)) <= (p / 2) / 2 by A27, XXREAL_0:2;
then A52: |.(integral (f,a,(a + (1 / (m + 1))))).| <= (p / 2) / 2 by A46, XXREAL_0:2;
|.(integral (f,(b - (1 / (m + 1))),b)).| <= (p / 2) / 2 by A50, A51, XXREAL_0:2;
then |.(integral (f,a,(a + (1 / (m + 1))))).| + |.(integral (f,(b - (1 / (m + 1))),b)).| <= ((p / 2) / 2) + ((p / 2) / 2) by A52, XREAL_1:7;
then |.((I . m) - (integral (f,a,b))).| <= p / 2 by A43, XXREAL_0:2;
hence |.((I . m) - (integral (f,a,b))).| < p by A16, XXREAL_0:2; :: thesis: verum

end;

hence I is convergent by SEQ_2:def 6; :: thesis: lim I = integral (f,a,b)
hence lim I = integral (f,a,b) by A15, SEQ_2:def 7; :: thesis: verum