let a, b be real number ; :: thesis: for H being Functional_Sequence of REAL ,REAL
for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] holds
( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
let H be Functional_Sequence of REAL ,REAL ; :: thesis: for rseq being Real_Sequence st a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] holds
( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
let rseq be Real_Sequence; :: thesis: ( a < b & ( for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) ) & H is_unif_conv_on ['a,b'] implies ( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b ) )
set AB = ['a,b'];
assume that
A1: a < b and
A2: for n being Element of NAT holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral (H . n),a,b ) and
A3: H is_unif_conv_on ['a,b'] ; :: thesis: ( (lim H,['a,b']) | ['a,b'] is bounded & lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
consider T being DivSequence of ['a,b'] such that
A4: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;
A5: ['a,b'] common_on_dom H by A3, SEQFUNC:44;
A6: for n being Element of NAT holds
( (H . n) || ['a,b'] is Function of ['a,b'],REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )

proof

let n be Element of NAT ; :: thesis: ( (H . n) || ['a,b'] is Function of ['a,b'],REAL & ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
['a,b'] c= dom (H . n) by A5, SEQFUNC:def 10;
hence A7: (H . n) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:131, INTEGRA5:6; :: thesis: ( ((H . n) || ['a,b']) | ['a,b'] is bounded & lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
thus ((H . n) || ['a,b']) | ['a,b'] is bounded by A2, INTEGRA5:9; :: thesis: ( lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) & lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
hence ( lower_sum ((H . n) || ['a,b']),T is convergent & lim (lower_sum ((H . n) || ['a,b']),T) = lower_integral ((H . n) || ['a,b']) & upper_sum ((H . n) || ['a,b']),T is convergent & lim (upper_sum ((H . n) || ['a,b']),T) = upper_integral ((H . n) || ['a,b']) ) by A4, A7, INTEGRA4:8, INTEGRA4:9; :: thesis: ( lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) & rseq . n = integral ((H . n) || ['a,b']) )
H . n is_integrable_on ['a,b'] by A2;
then (H . n) || ['a,b'] is integrable by INTEGRA5:def 2;
hence lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) by INTEGRA1:def 17; :: thesis: rseq . n = integral ((H . n) || ['a,b'])
rseq . n = integral (H . n),a,b by A2;
then rseq . n = integral (H . n),['a,b'] by A1, INTEGRA5:def 5;
hence rseq . n = integral ((H . n) || ['a,b']) ; :: thesis: verum

end;

set L1 = lower_integral ((lim H,['a,b']) || ['a,b']);
set K1 = upper_integral ((lim H,['a,b']) || ['a,b']);
A8: 0 < b - a by A1, XREAL_1:52;
consider K being Element of NAT such that
A9: for n being Element of NAT
for x being Element of REAL st n >= K & x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < 1 by A3, SEQFUNC:44;
(H . K) | ['a,b'] is bounded by A2;
then consider r being real number such that
A10: for c being set st c in ['a,b'] /\ (dom (H . K)) holds
abs ((H . K) . c) <= r by RFUNCT_1:90;
set H0 = (lim H,['a,b']) || ['a,b'];
H is_point_conv_on ['a,b'] by A3, SEQFUNC:23;
then A11: dom (lim H,['a,b']) = ['a,b'] by SEQFUNC:22;
then A12: (lim H,['a,b']) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:131, INTEGRA5:6;
dom (lim H,['a,b']) c= dom (H . K) by A5, A11, SEQFUNC:def 10;
then A13: ['a,b'] /\ (dom (lim H,['a,b'])) c= ['a,b'] /\ (dom (H . K)) by XBOOLE_1:26;

now

let c be set ; :: thesis: ( c in ['a,b'] /\ (dom (lim H,['a,b'])) implies abs ((lim H,['a,b']) . c) <= r + 1 )
(lim H,['a,b']) . c = ((H . K) . c) - (((H . K) . c) - ((lim H,['a,b']) . c)) ;
then A14: abs ((lim H,['a,b']) . c) <= (abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim H,['a,b']) . c))) by COMPLEX1:143;
assume A15: c in ['a,b'] /\ (dom (lim H,['a,b'])) ; :: thesis: abs ((lim H,['a,b']) . c) <= r + 1
then c in ['a,b'] by XBOOLE_0:def 4;
then A16: abs (((H . K) . c) - ((lim H,['a,b']) . c)) < 1 by A9;
abs ((H . K) . c) <= r by A10, A13, A15;
then (abs ((H . K) . c)) + (abs (((H . K) . c) - ((lim H,['a,b']) . c))) <= r + 1 by A16, XREAL_1:9;
hence abs ((lim H,['a,b']) . c) <= r + 1 by A14, XXREAL_0:2; :: thesis: verum

end;

hence A17: (lim H,['a,b']) | ['a,b'] is bounded by RFUNCT_1:90; :: thesis: ( lim H,['a,b'] is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
then A18: ((lim H,['a,b']) || ['a,b']) | ['a,b'] is bounded_above by INTEGRA5:7;
A19: ((lim H,['a,b']) || ['a,b']) | ['a,b'] is bounded_below by A17, INTEGRA5:8;
then A20: upper_sum ((lim H,['a,b']) || ['a,b']),T is convergent by A4, A18, A12, INTEGRA4:9;
A21: for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)

proof

let e be Element of REAL ; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
then consider N being Element of NAT such that
A22: for n being Element of NAT
for x being Element of REAL st n >= N & x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < e by A3, SEQFUNC:44;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)

now

let n, k be Element of NAT ; :: thesis: ( N <= n implies abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
reconsider Tk = T . k as Division of ['a,b'] ;
set l0 = len Tk;
A23: dom Tk = Seg (len Tk) by FINSEQ_1:def 3;
set Hn = (H . n) || ['a,b'];
len (upper_volume ((H . n) || ['a,b']),(T . k)) = len Tk by INTEGRA1:def 7;
then reconsider R1 = upper_volume ((H . n) || ['a,b']),(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
len (upper_volume ((lim H,['a,b']) || ['a,b']),(T . k)) = len Tk by INTEGRA1:def 7;
then reconsider R2 = upper_volume ((lim H,['a,b']) || ['a,b']),(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - ((upper_sum ((H . n) || ['a,b']),T) . k) by INTEGRA2:def 4;
then ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - (upper_sum ((H . n) || ['a,b']),(T . k)) by INTEGRA2:def 4;
then A24: ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) = Sum (R2 - R1) by RVSUM_1:120;
consider H1 being Function of ['a,b'],REAL such that
A25: rng H1 = {e} and
A26: H1 | ['a,b'] is bounded by INTEGRA4:5;
len (upper_volume H1,(T . k)) = len Tk by INTEGRA1:def 7;
then reconsider R3 = upper_volume H1,(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
A27: vol ['a,b'] = b - a by A1, INTEGRA6:5;
upper_bound (rng H1) = e by A25, SEQ_4:22;
then A28: upper_sum H1,(T . k) <= e * (b - a) by A26, A27, INTEGRA1:29;
assume A29: N <= n ; :: thesis: abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
A30: for i being Element of NAT st i in dom Tk holds
( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )

proof

let i be Element of NAT ; :: thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) )
A31: 0 <= vol (divset (T . k),i) by INTEGRA1:11;
assume A32: i in dom Tk ; :: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
A33: ( (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) & (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) )

proof

A34: divset (T . k),i c= ['a,b'] by A32, INTEGRA1:10;
then reconsider g = ((lim H,['a,b']) || ['a,b']) | (divset (T . k),i) as Function of (divset (T . k),i),REAL by A12, FUNCT_2:38;
consider x0 being set such that
A35: x0 in divset (T . k),i by XBOOLE_0:def 1;
(H . n) || ['a,b'] is Function of ['a,b'],REAL by A6;
then reconsider f = ((H . n) || ['a,b']) | (divset (T . k),i) as Function of (divset (T . k),i),REAL by A34, FUNCT_2:38;
A36: for x being set st x in divset (T . k),i holds
abs ((f . x) - (g . x)) <= e

proof

let x be set ; :: thesis: ( x in divset (T . k),i implies abs ((f . x) - (g . x)) <= e )
assume A37: x in divset (T . k),i ; :: thesis: abs ((f . x) - (g . x)) <= e
then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x)) by FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim H,['a,b']) || ['a,b']) . x)) by A37, FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim H,['a,b']) || ['a,b']) . x)) by A34, A37, FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim H,['a,b']) . x)) by A34, A37, FUNCT_1:72;
hence abs ((f . x) - (g . x)) <= e by A22, A29, A34, A37; :: thesis: verum

end;

((H . n) || ['a,b']) | ['a,b'] is bounded by A6;
then f | (divset (T . k),i) is bounded_above by A32, INTEGRA1:10, INTEGRA2:5;
then A38: rng f is bounded_above by INTEGRA1:15;
H1 . x0 in {e} by A25, A34, A35, FUNCT_2:6;
then H1 . x0 = e by TARSKI:def 1;
then A39: (H1 | (divset (T . k),i)) . x0 = e by A35, FUNCT_1:72;
H1 | (divset (T . k),i) is Function of (divset (T . k),i),REAL by A34, FUNCT_2:38;
then e in rng (H1 | (divset (T . k),i)) by A35, A39, FUNCT_2:6;
then A40: {e} c= rng (H1 | (divset (T . k),i)) by ZFMISC_1:37;
rng (H1 | (divset (T . k),i)) c= {e} by A25, RELAT_1:99;
then rng (H1 | (divset (T . k),i)) = {e} by A40, XBOOLE_0:def 10;
then A41: e = upper_bound (rng (H1 | (divset (T . k),i))) by SEQ_4:22;
g | (divset (T . k),i) is bounded_above by A18, A32, INTEGRA1:10, INTEGRA2:5;
then A42: rng g is bounded_above by INTEGRA1:15;
hence (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) by A38, A41, A36, Th1; :: thesis: (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i)))
for x being set st x in divset (T . k),i holds
abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset (T . k),i)))

proof

let x be set ; :: thesis: ( x in divset (T . k),i implies abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset (T . k),i))) )
assume x in divset (T . k),i ; :: thesis: abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset (T . k),i)))
then abs ((f . x) - (g . x)) <= upper_bound (rng (H1 | (divset (T . k),i))) by A41, A36;
hence abs ((g . x) - (f . x)) <= upper_bound (rng (H1 | (divset (T . k),i))) by COMPLEX1:146; :: thesis: verum

end;

hence (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= upper_bound (rng (H1 | (divset (T . k),i))) by A38, A42, Th1; :: thesis: verum

end;

(R1 - R2) . i = (R1 . i) - (R2 . i) by RVSUM_1:48;
then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_volume ((lim H,['a,b']) || ['a,b']),(T . k)) . i) by A32, INTEGRA1:def 7;
then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) by A32, INTEGRA1:def 7;
then (R1 - R2) . i = ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i)) ;
then (R1 - R2) . i <= (upper_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i)) by A33, A31, XREAL_1:66;
hence (R1 - R2) . i <= R3 . i by A32, INTEGRA1:def 7; :: thesis: (R2 - R1) . i <= R3 . i
(R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:48;
then (R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_volume ((H . n) || ['a,b']),(T . k)) . i) by A32, INTEGRA1:def 7;
then (R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) by A32, INTEGRA1:def 7;
then (R2 - R1) . i = ((upper_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (upper_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i)) ;
then (R2 - R1) . i <= (upper_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i)) by A33, A31, XREAL_1:66;
hence (R2 - R1) . i <= R3 . i by A32, INTEGRA1:def 7; :: thesis: verum

end;

then for i being Nat st i in dom Tk holds
(R2 - R1) . i <= R3 . i ;
then ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) <= Sum R3 by A23, A24, RVSUM_1:112;
then ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k) <= e * (b - a) by A28, XXREAL_0:2;
then A43: - (e * (b - a)) <= - (((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((upper_sum ((H . n) || ['a,b']),T) . k)) by XREAL_1:26;
((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (upper_sum ((H . n) || ['a,b']),(T . k)) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) by INTEGRA2:def 4;
then ((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (upper_sum ((H . n) || ['a,b']),(T . k)) - (upper_sum ((lim H,['a,b']) || ['a,b']),(T . k)) by INTEGRA2:def 4;
then A44: ((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) = Sum (R1 - R2) by RVSUM_1:120;
for i being Nat st i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i by A23, A30;
then ((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= Sum R3 by A44, RVSUM_1:112;
then ((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= e * (b - a) by A28, XXREAL_0:2;
hence abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) by A43, ABSVALUE:12; :: thesis: verum

end;

hence for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) ; :: thesis: verum

end;

A45: for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e

proof

let e be Element of REAL ; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e )
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e
then consider N being Element of NAT such that
A46: for n, k being Element of NAT st N <= n holds
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a) by A21, A8, XREAL_1:141;
take N ; :: thesis: for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e

A47: now

let n, k be Element of NAT ; :: thesis: ( N <= n implies abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )
assume N <= n ; :: thesis: abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
then abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a) by A46;
hence abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e by A8, XCMPLX_1:88; :: thesis: verum

end;

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( N <= n implies abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e )
assume A48: N <= n ; :: thesis: abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e

A49: now

let k be Element of NAT ; :: thesis: (abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
abs (((upper_sum ((H . n) || ['a,b']),T) . k) - ((upper_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e by A47, A48;
then abs (((upper_sum ((H . n) || ['a,b']),T) . k) + ((- (upper_sum ((lim H,['a,b']) || ['a,b']),T)) . k)) <= e by SEQ_1:14;
then abs (((upper_sum ((H . n) || ['a,b']),T) + (- (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k) <= e by SEQ_1:11;
hence (abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e by SEQ_1:16; :: thesis: verum

end;

A50: upper_sum ((H . n) || ['a,b']),T is convergent by A6;
then lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (lim (upper_sum ((H . n) || ['a,b']),T)) - (lim (upper_sum ((lim H,['a,b']) || ['a,b']),T)) by A20, SEQ_2:26;
then lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (upper_integral ((H . n) || ['a,b'])) - (lim (upper_sum ((lim H,['a,b']) || ['a,b']),T)) by A6;
then A51: lim ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) = (upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])) by A4, A18, A19, A12, INTEGRA4:9;
A52: (upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T) is convergent by A20, A50, SEQ_2:25;
then abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T)) is convergent by SEQ_4:26;
then lim (abs ((upper_sum ((H . n) || ['a,b']),T) - (upper_sum ((lim H,['a,b']) || ['a,b']),T))) <= e by A49, PREPOWER:3;
hence abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e by A52, A51, SEQ_4:27; :: thesis: verum

end;

end;

A53: lower_sum ((lim H,['a,b']) || ['a,b']),T is convergent by A4, A18, A19, A12, INTEGRA4:8;
A54: for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)

proof

let e be Element of REAL ; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
then consider N being Element of NAT such that
A55: for n being Element of NAT
for x being Element of REAL st n >= N & x in ['a,b'] holds
abs (((H . n) . x) - ((lim H,['a,b']) . x)) < e by A3, SEQFUNC:44;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)

hereby :: thesis: verum

let n, k be Element of NAT ; :: thesis: ( N <= n implies abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) )
set Hn = (H . n) || ['a,b'];
reconsider Tk = T . k as Division of ['a,b'] ;
set l0 = len Tk;
consider H1 being Function of ['a,b'],REAL such that
A56: rng H1 = {e} and
A57: H1 | ['a,b'] is bounded by INTEGRA4:5;
A58: lower_sum H1,(T . k) <= upper_sum H1,(T . k) by A57, INTEGRA1:30;
len (lower_volume ((lim H,['a,b']) || ['a,b']),(T . k)) = len Tk by INTEGRA1:def 8;
then reconsider R2 = lower_volume ((lim H,['a,b']) || ['a,b']),(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
len (lower_volume ((H . n) || ['a,b']),(T . k)) = len Tk by INTEGRA1:def 8;
then reconsider R1 = lower_volume ((H . n) || ['a,b']),(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
len (lower_volume H1,(T . k)) = len Tk by INTEGRA1:def 8;
then reconsider R3 = lower_volume H1,(T . k) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:110;
assume A59: N <= n ; :: thesis: abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a)
A60: for i being Element of NAT st i in dom Tk holds
( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )

proof

let i be Element of NAT ; :: thesis: ( i in dom Tk implies ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i ) )
consider x0 being set such that
A61: x0 in divset (T . k),i by XBOOLE_0:def 1;
A62: rng (H1 | (divset (T . k),i)) c= {e} by A56, RELAT_1:99;
assume A63: i in dom Tk ; :: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
then A64: divset (T . k),i c= ['a,b'] by INTEGRA1:10;
then reconsider g = ((lim H,['a,b']) || ['a,b']) | (divset (T . k),i) as Function of (divset (T . k),i),REAL by A12, FUNCT_2:38;
(H . n) || ['a,b'] is Function of ['a,b'],REAL by A6;
then reconsider f = ((H . n) || ['a,b']) | (divset (T . k),i) as Function of (divset (T . k),i),REAL by A64, FUNCT_2:38;
A65: 0 <= vol (divset (T . k),i) by INTEGRA1:11;
H1 . x0 in {e} by A56, A64, A61, FUNCT_2:6;
then H1 . x0 = e by TARSKI:def 1;
then A66: (H1 | (divset (T . k),i)) . x0 = e by A61, FUNCT_1:72;
H1 | (divset (T . k),i) is Function of (divset (T . k),i),REAL by A64, FUNCT_2:38;
then e in rng (H1 | (divset (T . k),i)) by A61, A66, FUNCT_2:6;
then {e} c= rng (H1 | (divset (T . k),i)) by ZFMISC_1:37;
then rng (H1 | (divset (T . k),i)) = {e} by A62, XBOOLE_0:def 10;
then A67: e = lower_bound (rng (H1 | (divset (T . k),i))) by SEQ_4:22;

A68: now

let x be set ; :: thesis: ( x in divset (T . k),i implies abs ((f . x) - (g . x)) <= e )
assume A69: x in divset (T . k),i ; :: thesis: abs ((f . x) - (g . x)) <= e
then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (g . x)) by FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs ((((H . n) || ['a,b']) . x) - (((lim H,['a,b']) || ['a,b']) . x)) by A69, FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs (((H . n) . x) - (((lim H,['a,b']) || ['a,b']) . x)) by A64, A69, FUNCT_1:72;
then abs ((f . x) - (g . x)) = abs (((H . n) . x) - ((lim H,['a,b']) . x)) by A64, A69, FUNCT_1:72;
hence abs ((f . x) - (g . x)) <= e by A55, A59, A64, A69; :: thesis: verum

end;

(R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:48;
then (R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_volume ((H . n) || ['a,b']),(T . k)) . i) by A63, INTEGRA1:def 8;
then (R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) by A63, INTEGRA1:def 8;
then A70: (R2 - R1) . i = ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i)) ;
(R1 - R2) . i = (R1 . i) - (R2 . i) by RVSUM_1:48;
then (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_volume ((lim H,['a,b']) || ['a,b']),(T . k)) . i) by A63, INTEGRA1:def 8;
then (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) - ((lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) * (vol (divset (T . k),i))) by A63, INTEGRA1:def 8;
then A71: (R1 - R2) . i = ((lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i))))) * (vol (divset (T . k),i)) ;
((H . n) || ['a,b']) | ['a,b'] is bounded by A6;
then f | (divset (T . k),i) is bounded_below by A63, INTEGRA1:10, INTEGRA2:6;
then A72: rng f is bounded_below by INTEGRA1:13;
g | (divset (T . k),i) is bounded_below by A19, A63, INTEGRA1:10, INTEGRA2:6;
then A73: rng g is bounded_below by INTEGRA1:13;
then (lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) <= lower_bound (rng (H1 | (divset (T . k),i))) by A72, A67, A68, Th2;
then (R1 - R2) . i <= (lower_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i)) by A71, A65, XREAL_1:66;
hence (R1 - R2) . i <= R3 . i by A63, INTEGRA1:def 8; :: thesis: (R2 - R1) . i <= R3 . i

now

let x be set ; :: thesis: ( x in divset (T . k),i implies abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset (T . k),i))) )
assume x in divset (T . k),i ; :: thesis: abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset (T . k),i)))
then abs ((f . x) - (g . x)) <= lower_bound (rng (H1 | (divset (T . k),i))) by A67, A68;
hence abs ((g . x) - (f . x)) <= lower_bound (rng (H1 | (divset (T . k),i))) by COMPLEX1:146; :: thesis: verum

end;

then (lower_bound (rng (((lim H,['a,b']) || ['a,b']) | (divset (T . k),i)))) - (lower_bound (rng (((H . n) || ['a,b']) | (divset (T . k),i)))) <= lower_bound (rng (H1 | (divset (T . k),i))) by A72, A73, Th2;
then (R2 - R1) . i <= (lower_bound (rng (H1 | (divset (T . k),i)))) * (vol (divset (T . k),i)) by A70, A65, XREAL_1:66;
hence (R2 - R1) . i <= R3 . i by A63, INTEGRA1:def 8; :: thesis: verum

end;

((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (lower_sum ((H . n) || ['a,b']),(T . k)) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) by INTEGRA2:def 5;
then ((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = (lower_sum ((H . n) || ['a,b']),(T . k)) - (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k)) by INTEGRA2:def 5;
then A74: ((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) = Sum (R1 - R2) by RVSUM_1:120;
A75: vol ['a,b'] = b - a by A1, INTEGRA6:5;
upper_bound (rng H1) = e by A56, SEQ_4:22;
then upper_sum H1,(T . k) <= e * (b - a) by A57, A75, INTEGRA1:29;
then A76: lower_sum H1,(T . k) <= e * (b - a) by A58, XXREAL_0:2;
((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - ((lower_sum ((H . n) || ['a,b']),T) . k) by INTEGRA2:def 5;
then ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = (lower_sum ((lim H,['a,b']) || ['a,b']),(T . k)) - (lower_sum ((H . n) || ['a,b']),(T . k)) by INTEGRA2:def 5;
then A77: ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) = Sum (R2 - R1) by RVSUM_1:120;
A78: Seg (len Tk) = dom Tk by FINSEQ_1:def 3;
then for i being Nat st i in Seg (len Tk) holds
(R2 - R1) . i <= R3 . i by A60;
then ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) <= Sum R3 by A77, RVSUM_1:112;
then ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k) <= e * (b - a) by A76, XXREAL_0:2;
then A79: - (e * (b - a)) <= - (((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) - ((lower_sum ((H . n) || ['a,b']),T) . k)) by XREAL_1:26;
for i being Nat st i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i by A78, A60;
then ((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= lower_sum H1,(T . k) by A74, RVSUM_1:112;
then ((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k) <= e * (b - a) by A76, XXREAL_0:2;
hence abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e * (b - a) by A79, ABSVALUE:12; :: thesis: verum

end;

end;

A80: for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e

proof

let e be Element of REAL ; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
then consider N being Element of NAT such that
A81: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a) by A54, A8, XREAL_1:141;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e

hereby :: thesis: verum

let n, k be Element of NAT ; :: thesis: ( N <= n implies abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e )
assume N <= n ; :: thesis: abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e
then abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= (e / (b - a)) * (b - a) by A81;
hence abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e by A8, XCMPLX_1:88; :: thesis: verum

end;

end;

A82: for e being Element of REAL st 0 < e holds
ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e

proof

let e be Element of REAL ; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e )
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e
then consider N being Element of NAT such that
A83: for n, k being Element of NAT st N <= n holds
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e by A80;
take N ; :: thesis: for n being Element of NAT st N <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( N <= n implies abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e )
set LHT = lower_sum ((H . n) || ['a,b']),T;
assume A84: N <= n ; :: thesis: abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e

A85: now

let k be Element of NAT ; :: thesis: (abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e
abs (((lower_sum ((H . n) || ['a,b']),T) . k) - ((lower_sum ((lim H,['a,b']) || ['a,b']),T) . k)) <= e by A83, A84;
then abs (((lower_sum ((H . n) || ['a,b']),T) . k) + ((- (lower_sum ((lim H,['a,b']) || ['a,b']),T)) . k)) <= e by SEQ_1:14;
then abs (((lower_sum ((H . n) || ['a,b']),T) + (- (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k) <= e by SEQ_1:11;
hence (abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) . k <= e by SEQ_1:16; :: thesis: verum

end;

A86: lower_sum ((H . n) || ['a,b']),T is convergent by A6;
then lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lim (lower_sum ((H . n) || ['a,b']),T)) - (lim (lower_sum ((lim H,['a,b']) || ['a,b']),T)) by A53, SEQ_2:26;
then lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lower_integral ((H . n) || ['a,b'])) - (lim (lower_sum ((lim H,['a,b']) || ['a,b']),T)) by A6;
then A87: lim ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) = (lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b'])) by A4, A18, A19, A12, INTEGRA4:8;
A88: (lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T) is convergent by A53, A86, SEQ_2:25;
then abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T)) is convergent by SEQ_4:26;
then lim (abs ((lower_sum ((H . n) || ['a,b']),T) - (lower_sum ((lim H,['a,b']) || ['a,b']),T))) <= e by A85, PREPOWER:3;
hence abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= e by A87, A88, SEQ_4:27; :: thesis: verum

end;

end;

A89: now

let e1 be Element of REAL ; :: thesis: ( 0 < e1 implies abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1 )
set e = e1 / 2;
assume A90: 0 < e1 ; :: thesis: abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1
then A91: 0 < e1 / 2 by XREAL_1:217;
then consider N1 being Element of NAT such that
A92: for n being Element of NAT st N1 <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2 by A45, XREAL_1:217;
consider N2 being Element of NAT such that
A93: for n being Element of NAT st N2 <= n holds
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2 by A82, A91, XREAL_1:217;
reconsider n = max N1,N2 as Element of NAT by XXREAL_0:16;
set K = upper_integral ((H . n) || ['a,b']);
set L = lower_integral ((H . n) || ['a,b']);
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2 by A93, XXREAL_0:25;
then A94: abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2 by A6;
((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) - ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b']))) = (lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])) ;
then A95: abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b'])))) by COMPLEX1:143;
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= (e1 / 2) / 2 by A92, XXREAL_0:25;
then (abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim H,['a,b']) || ['a,b'])))) <= ((e1 / 2) / 2) + ((e1 / 2) / 2) by A94, XREAL_1:9;
then A96: abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= e1 / 2 by A95, XXREAL_0:2;
e1 / 2 < e1 by A90, XREAL_1:218;
hence abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) < e1 by A96, XXREAL_0:2; :: thesis: verum

end;

A97: now

assume upper_integral ((lim H,['a,b']) || ['a,b']) <> lower_integral ((lim H,['a,b']) || ['a,b']) ; :: thesis: contradiction
then 0 < abs ((lower_integral ((lim H,['a,b']) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) by COMPLEX1:148;
hence contradiction by A89; :: thesis: verum

end;

( (lim H,['a,b']) || ['a,b'] is upper_integrable & (lim H,['a,b']) || ['a,b'] is lower_integrable ) by A18, A19, A12, INTEGRA4:10;
then (lim H,['a,b']) || ['a,b'] is integrable by A97, INTEGRA1:def 17;
hence lim H,['a,b'] is_integrable_on ['a,b'] by INTEGRA5:def 2; :: thesis: ( rseq is convergent & lim rseq = integral (lim H,['a,b']),a,b )
A98: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p )
set e = p / 2;
assume A99: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p
then consider N being Element of NAT such that
A100: for n being Element of NAT st N <= n holds
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= p / 2 by A45, XREAL_1:217;
take N ; :: thesis: for m being Element of NAT st N <= m holds
abs ((rseq . m) - (integral (lim H,['a,b']),a,b)) < p
A101: p / 2 < p by A99, XREAL_1:218;

hereby :: thesis: verum

let n be Element of NAT ; :: thesis: ( N <= n implies abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < p )
upper_integral ((H . n) || ['a,b']) = integral ((H . n) || ['a,b']) ;
then A102: upper_integral ((H . n) || ['a,b']) = rseq . n by A6;
upper_integral ((lim H,['a,b']) || ['a,b']) = integral (lim H,['a,b']),['a,b'] ;
then A103: upper_integral ((lim H,['a,b']) || ['a,b']) = integral (lim H,['a,b']),a,b by A1, INTEGRA5:def 5;
assume N <= n ; :: thesis: abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < p
then abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim H,['a,b']) || ['a,b']))) <= p / 2 by A100;
hence abs ((rseq . n) - (integral (lim H,['a,b']),a,b)) < p by A101, A102, A103, XXREAL_0:2; :: thesis: verum

end;

end;

hence rseq is convergent by SEQ_2:def 6; :: thesis: lim rseq = integral (lim H,['a,b']),a,b
hence lim rseq = integral (lim H,['a,b']),a,b by A98, SEQ_2:def 7; :: thesis: verum