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