let a, b be Real; :: 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: for n being Nat holds
( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) )

proof

let n be Nat; :: thesis: ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) )
n in NAT by ORDINAL1:def 12;
hence ( H . n is_integrable_on ['a,b'] & (H . n) | ['a,b'] is bounded & rseq . n = integral ((H . n),a,b) ) by A2; :: thesis: verum

end;

A6: ['a,b'] common_on_dom H by A3, SEQFUNC:43;
A7: 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 A6, SEQFUNC:def 9;
hence A8: (H . n) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:68, 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; :: 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, A8, 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 ;
hence lower_integral ((H . n) || ['a,b']) = upper_integral ((H . n) || ['a,b']) ; :: 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 4;
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']);
A9: 0 < b - a by A1, XREAL_1:50;
reconsider jj = 1 as Real ;
consider K being Nat such that
A10: for n being Nat
for x being Element of REAL st n >= K & x in ['a,b'] holds
|.(((H . n) . x) - ((lim (H,['a,b'])) . x)).| < jj by A3, SEQFUNC:43;
(H . K) | ['a,b'] is bounded by A5;
then consider r being Real such that
A11: for c being object st c in ['a,b'] /\ (dom (H . K)) holds
|.((H . K) . c).| <= r by RFUNCT_1:73;
set H0 = (lim (H,['a,b'])) || ['a,b'];
H is_point_conv_on ['a,b'] by A3, SEQFUNC:22;
then A12: dom (lim (H,['a,b'])) = ['a,b'] by SEQFUNC:21;
then A13: (lim (H,['a,b'])) || ['a,b'] is Function of ['a,b'],REAL by FUNCT_2:68, INTEGRA5:6;
dom (lim (H,['a,b'])) c= dom (H . K) by A6, A12, SEQFUNC:def 9;
then A14: ['a,b'] /\ (dom (lim (H,['a,b']))) c= ['a,b'] /\ (dom (H . K)) by XBOOLE_1:26;

now :: thesis: for c being object st c in ['a,b'] /\ (dom (lim (H,['a,b']))) holds
|.((lim (H,['a,b'])) . c).| <= r + 1

let c be object ; :: thesis: ( c in ['a,b'] /\ (dom (lim (H,['a,b']))) implies |.((lim (H,['a,b'])) . c).| <= r + 1 )
(lim (H,['a,b'])) . c = ((H . K) . c) - (((H . K) . c) - ((lim (H,['a,b'])) . c)) ;
then A15: |.((lim (H,['a,b'])) . c).| <= |.((H . K) . c).| + |.(((H . K) . c) - ((lim (H,['a,b'])) . c)).| by COMPLEX1:57;
assume A16: c in ['a,b'] /\ (dom (lim (H,['a,b']))) ; :: thesis: |.((lim (H,['a,b'])) . c).| <= r + 1
then c in ['a,b'] by XBOOLE_0:def 4;
then A17: |.(((H . K) . c) - ((lim (H,['a,b'])) . c)).| < 1 by A10;
|.((H . K) . c).| <= r by A11, A14, A16;
then |.((H . K) . c).| + |.(((H . K) . c) - ((lim (H,['a,b'])) . c)).| <= r + 1 by A17, XREAL_1:7;
hence |.((lim (H,['a,b'])) . c).| <= r + 1 by A15, XXREAL_0:2; :: thesis: verum

end;

hence A18: (lim (H,['a,b'])) | ['a,b'] is bounded by RFUNCT_1:73; :: thesis: ( lim (H,['a,b']) is_integrable_on ['a,b'] & rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) )
then A19: ((lim (H,['a,b'])) || ['a,b']) | ['a,b'] is bounded_above ;
A20: ((lim (H,['a,b'])) || ['a,b']) | ['a,b'] is bounded_below by A18;
then A21: upper_sum (((lim (H,['a,b'])) || ['a,b']),T) is convergent by A4, A19, A13, INTEGRA4:9;
A22: for e being Real st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
|.(((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 Real; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
|.(((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
|.(((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 Nat such that
A23: for n being Nat
for x being Element of REAL st n >= N & x in ['a,b'] holds
|.(((H . n) . x) - ((lim (H,['a,b'])) . x)).| < e by A3, SEQFUNC:43;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
|.(((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e * (b - a)
let n, k be Element of NAT ; :: thesis: ( N <= n implies |.(((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;
A24: 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 6;
then reconsider R1 = upper_volume (((H . n) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
len (upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def 6;
then reconsider R2 = upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
((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 2;
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 2;
then A25: ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) = Sum (R2 - R1) by RVSUM_1:90;
consider H1 being Function of ['a,b'],REAL such that
A26: rng H1 = {e} and
A27: H1 | ['a,b'] is bounded by INTEGRA4:5;
len (upper_volume (H1,(T . k))) = len Tk by INTEGRA1:def 6;
then reconsider R3 = upper_volume (H1,(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
A28: vol ['a,b'] = b - a by A1, INTEGRA6:5;
upper_bound (rng H1) = e by A26, SEQ_4:9;
then A29: upper_sum (H1,(T . k)) <= e * (b - a) by A27, A28, INTEGRA1:27;
assume A30: N <= n ; :: thesis: |.(((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e * (b - a)
A31: 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 ) )
A32: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9;
assume A33: i in dom Tk ; :: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
A34: ( (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

A35: divset ((T . k),i) c= ['a,b'] by A33, INTEGRA1:8;
then reconsider g = ((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A13, FUNCT_2:32;
consider x0 being object such that
A36: x0 in divset ((T . k),i) by XBOOLE_0:def 1;
(H . n) || ['a,b'] is Function of ['a,b'],REAL by A7;
then reconsider f = ((H . n) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A35, FUNCT_2:32;
A37: for x being set st x in divset ((T . k),i) holds
|.((f . x) - (g . x)).| <= e

proof

let x be set ; :: thesis: ( x in divset ((T . k),i) implies |.((f . x) - (g . x)).| <= e )
assume A38: x in divset ((T . k),i) ; :: thesis: |.((f . x) - (g . x)).| <= e
then |.((f . x) - (g . x)).| = |.((((H . n) || ['a,b']) . x) - (g . x)).| by FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.((((H . n) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)).| by A38, FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)).| by A35, A38, FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.(((H . n) . x) - ((lim (H,['a,b'])) . x)).| by A35, A38, FUNCT_1:49;
hence |.((f . x) - (g . x)).| <= e by A23, A30, A35, A38; :: thesis: verum

end;

((H . n) || ['a,b']) | ['a,b'] is bounded by A7;
then f | (divset ((T . k),i)) is bounded_above by A33, INTEGRA1:8, INTEGRA2:5;
then A39: rng f is bounded_above by INTEGRA1:13;
H1 . x0 in {e} by A26, A35, A36, FUNCT_2:4;
then H1 . x0 = e by TARSKI:def 1;
then A40: (H1 | (divset ((T . k),i))) . x0 = e by A36, FUNCT_1:49;
H1 | (divset ((T . k),i)) is Function of (divset ((T . k),i)),REAL by A35, FUNCT_2:32;
then e in rng (H1 | (divset ((T . k),i))) by A36, A40, FUNCT_2:4;
then A41: {e} c= rng (H1 | (divset ((T . k),i))) by ZFMISC_1:31;
rng (H1 | (divset ((T . k),i))) c= {e} by A26, RELAT_1:70;
then rng (H1 | (divset ((T . k),i))) = {e} by A41, XBOOLE_0:def 10;
then A42: e = upper_bound (rng (H1 | (divset ((T . k),i)))) by SEQ_4:9;
g | (divset ((T . k),i)) is bounded_above by A19, A33, INTEGRA1:8, INTEGRA2:5;
then A43: rng g is bounded_above by INTEGRA1:13;
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 A39, A42, A37, 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
|.((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 |.((g . x) - (f . x)).| <= upper_bound (rng (H1 | (divset ((T . k),i)))) )
assume x in divset ((T . k),i) ; :: thesis: |.((g . x) - (f . x)).| <= upper_bound (rng (H1 | (divset ((T . k),i))))
then |.((f . x) - (g . x)).| <= upper_bound (rng (H1 | (divset ((T . k),i)))) by A42, A37;
hence |.((g . x) - (f . x)).| <= upper_bound (rng (H1 | (divset ((T . k),i)))) by COMPLEX1:60; :: 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 A39, A43, Th1; :: thesis: verum

end;

(R1 - R2) . i = (R1 . i) - (R2 . i) by RVSUM_1:27;
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 A33, INTEGRA1:def 6;
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 A33, INTEGRA1:def 6;
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 A34, A32, XREAL_1:64;
hence (R1 - R2) . i <= R3 . i by A33, INTEGRA1:def 6; :: thesis: (R2 - R1) . i <= R3 . i
(R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:27;
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 A33, INTEGRA1:def 6;
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 A33, INTEGRA1:def 6;
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 A34, A32, XREAL_1:64;
hence (R2 - R1) . i <= R3 . i by A33, INTEGRA1:def 6; :: 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 A24, A25, RVSUM_1:82;
then ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k) <= e * (b - a) by A29, XXREAL_0:2;
then A44: - (e * (b - a)) <= - (((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((upper_sum (((H . n) || ['a,b']),T)) . k)) by XREAL_1:24;
((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 2;
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 2;
then A45: ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = Sum (R1 - R2) by RVSUM_1:90;
for i being Nat st i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i by A24, A31;
then ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= Sum R3 by A45, RVSUM_1:82;
then ((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= e * (b - a) by A29, XXREAL_0:2;
hence |.(((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e * (b - a) by A44, ABSVALUE:5; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e )
reconsider ee = e as Real ;
assume 0 < e ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st N <= n holds
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e
then consider N being Element of NAT such that
A47: for n, k being Element of NAT st N <= n holds
|.(((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= (ee / (b - a)) * (b - a) by A22, A9, XREAL_1:139;
take N ; :: thesis: for n being Element of NAT st N <= n holds
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e

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

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

end;

hereby :: thesis: verum

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

A50: now :: thesis: for k being Nat holds |.((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))).| . k <= e

let k be Nat; :: thesis: |.((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))).| . k <= e
k in NAT by ORDINAL1:def 12;
then |.(((upper_sum (((H . n) || ['a,b']),T)) . k) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e by A48, A49;
then |.(((upper_sum (((H . n) || ['a,b']),T)) . k) + ((- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) . k)).| <= e by SEQ_1:10;
then |.(((upper_sum (((H . n) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k).| <= e by SEQ_1:7;
hence |.((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))).| . k <= e by SEQ_1:12; :: thesis: verum

end;

A51: upper_sum (((H . n) || ['a,b']),T) is convergent by A7;
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 A21, SEQ_2:12;
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 A7;
then A52: 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, A19, A20, A13, INTEGRA4:9;
A53: (upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is convergent by A21, A51;
then abs ((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is convergent by SEQ_4:13;
then lim |.((upper_sum (((H . n) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))).| <= e by A50, PREPOWER:2;
hence |.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e by A53, A52, SEQ_4:14; :: thesis: verum

end;

end;

A54: lower_sum (((lim (H,['a,b'])) || ['a,b']),T) is convergent by A4, A19, A20, A13, INTEGRA4:8;
A55: for e being Real st 0 < e holds
ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
|.(((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 Real; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
|.(((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
|.(((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 Nat such that
A56: for n being Nat
for x being Element of REAL st n >= N & x in ['a,b'] holds
|.(((H . n) . x) - ((lim (H,['a,b'])) . x)).| < e by A3, SEQFUNC:43;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
|.(((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 |.(((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
A57: rng H1 = {e} and
A58: H1 | ['a,b'] is bounded by INTEGRA4:5;
A59: lower_sum (H1,(T . k)) <= upper_sum (H1,(T . k)) by A58, INTEGRA1:28;
len (lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def 7;
then reconsider R2 = lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
len (lower_volume (((H . n) || ['a,b']),(T . k))) = len Tk by INTEGRA1:def 7;
then reconsider R1 = lower_volume (((H . n) || ['a,b']),(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
len (lower_volume (H1,(T . k))) = len Tk by INTEGRA1:def 7;
then reconsider R3 = lower_volume (H1,(T . k)) as Element of (len Tk) -tuples_on REAL by FINSEQ_2:92;
assume A60: N <= n ; :: thesis: |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e * (b - a)
A61: 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 object such that
A62: x0 in divset ((T . k),i) by XBOOLE_0:def 1;
A63: rng (H1 | (divset ((T . k),i))) c= {e} by A57, RELAT_1:70;
assume A64: i in dom Tk ; :: thesis: ( (R1 - R2) . i <= R3 . i & (R2 - R1) . i <= R3 . i )
then A65: divset ((T . k),i) c= ['a,b'] by INTEGRA1:8;
then reconsider g = ((lim (H,['a,b'])) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A13, FUNCT_2:32;
(H . n) || ['a,b'] is Function of ['a,b'],REAL by A7;
then reconsider f = ((H . n) || ['a,b']) | (divset ((T . k),i)) as Function of (divset ((T . k),i)),REAL by A65, FUNCT_2:32;
A66: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9;
H1 . x0 in {e} by A57, A65, A62, FUNCT_2:4;
then H1 . x0 = e by TARSKI:def 1;
then A67: (H1 | (divset ((T . k),i))) . x0 = e by A62, FUNCT_1:49;
H1 | (divset ((T . k),i)) is Function of (divset ((T . k),i)),REAL by A65, FUNCT_2:32;
then e in rng (H1 | (divset ((T . k),i))) by A62, A67, FUNCT_2:4;
then {e} c= rng (H1 | (divset ((T . k),i))) by ZFMISC_1:31;
then rng (H1 | (divset ((T . k),i))) = {e} by A63, XBOOLE_0:def 10;
then A68: e = lower_bound (rng (H1 | (divset ((T . k),i)))) by SEQ_4:9;

A69: now :: thesis: for x being set st x in divset ((T . k),i) holds
|.((f . x) - (g . x)).| <= e

let x be set ; :: thesis: ( x in divset ((T . k),i) implies |.((f . x) - (g . x)).| <= e )
assume A70: x in divset ((T . k),i) ; :: thesis: |.((f . x) - (g . x)).| <= e
then |.((f . x) - (g . x)).| = |.((((H . n) || ['a,b']) . x) - (g . x)).| by FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.((((H . n) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)).| by A70, FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.(((H . n) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)).| by A65, A70, FUNCT_1:49;
then |.((f . x) - (g . x)).| = |.(((H . n) . x) - ((lim (H,['a,b'])) . x)).| by A65, A70, FUNCT_1:49;
hence |.((f . x) - (g . x)).| <= e by A56, A60, A65, A70; :: thesis: verum

end;

(R2 - R1) . i = (R2 . i) - (R1 . i) by RVSUM_1:27;
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 A64, INTEGRA1:def 7;
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 A64, INTEGRA1:def 7;
then A71: (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:27;
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 A64, INTEGRA1:def 7;
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 A64, INTEGRA1:def 7;
then A72: (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 A7;
then f | (divset ((T . k),i)) is bounded_below by A64, INTEGRA1:8, INTEGRA2:6;
then A73: rng f is bounded_below by INTEGRA1:11;
g | (divset ((T . k),i)) is bounded_below by A20, A64, INTEGRA1:8, INTEGRA2:6;
then A74: rng g is bounded_below by INTEGRA1:11;
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 A73, A68, A69, Th2;
then (R1 - R2) . i <= (lower_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A72, A66, XREAL_1:64;
hence (R1 - R2) . i <= R3 . i by A64, INTEGRA1:def 7; :: thesis: (R2 - R1) . i <= R3 . i

now :: thesis: for x being set st x in divset ((T . k),i) holds
|.((g . x) - (f . x)).| <= lower_bound (rng (H1 | (divset ((T . k),i))))

let x be set ; :: thesis: ( x in divset ((T . k),i) implies |.((g . x) - (f . x)).| <= lower_bound (rng (H1 | (divset ((T . k),i)))) )
assume x in divset ((T . k),i) ; :: thesis: |.((g . x) - (f . x)).| <= lower_bound (rng (H1 | (divset ((T . k),i))))
then |.((f . x) - (g . x)).| <= lower_bound (rng (H1 | (divset ((T . k),i)))) by A68, A69;
hence |.((g . x) - (f . x)).| <= lower_bound (rng (H1 | (divset ((T . k),i)))) by COMPLEX1:60; :: 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 A73, A74, Th2;
then (R2 - R1) . i <= (lower_bound (rng (H1 | (divset ((T . k),i))))) * (vol (divset ((T . k),i))) by A71, A66, XREAL_1:64;
hence (R2 - R1) . i <= R3 . i by A64, INTEGRA1:def 7; :: 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 3;
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 3;
then A75: ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) = Sum (R1 - R2) by RVSUM_1:90;
A76: vol ['a,b'] = b - a by A1, INTEGRA6:5;
upper_bound (rng H1) = e by A57, SEQ_4:9;
then upper_sum (H1,(T . k)) <= e * (b - a) by A58, A76, INTEGRA1:27;
then A77: lower_sum (H1,(T . k)) <= e * (b - a) by A59, 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 3;
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 3;
then A78: ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) = Sum (R2 - R1) by RVSUM_1:90;
A79: 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 A61;
then ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) <= Sum R3 by A78, RVSUM_1:82;
then ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k) <= e * (b - a) by A77, XXREAL_0:2;
then A80: - (e * (b - a)) <= - (((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) - ((lower_sum (((H . n) || ['a,b']),T)) . k)) by XREAL_1:24;
for i being Nat st i in Seg (len Tk) holds
(R1 - R2) . i <= R3 . i by A79, A61;
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 A75, RVSUM_1:82;
then ((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k) <= e * (b - a) by A77, XXREAL_0:2;
hence |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e * (b - a) by A80, ABSVALUE:5; :: thesis: verum

end;

end;

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

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n, k being Element of NAT st N <= n holds
|.(((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
|.(((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
A82: for n, k being Element of NAT st N <= n holds
|.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= (e / (b - a)) * (b - a) by A55, A9, XREAL_1:139;
take N ; :: thesis: for n, k being Element of NAT st N <= n holds
|.(((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 |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e )
assume N <= n ; :: thesis: |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e
then |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= (e / (b - a)) * (b - a) by A82;
hence |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e by A9, XCMPLX_1:87; :: thesis: verum

end;

end;

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

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Element of NAT st
for n being Element of NAT st N <= n holds
|.((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
|.((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e
then consider N being Element of NAT such that
A84: for n, k being Element of NAT st N <= n holds
|.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e by A81;
take N ; :: thesis: for n being Element of NAT st N <= n holds
|.((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 |.((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 A85: N <= n ; :: thesis: |.((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e

A86: now :: thesis: for k being Nat holds (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e

let k be Nat; :: thesis: (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e
k in NAT by ORDINAL1:def 12;
then |.(((lower_sum (((H . n) || ['a,b']),T)) . k) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . k)).| <= e by A84, A85;
then |.(((lower_sum (((H . n) || ['a,b']),T)) . k) + ((- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) . k)).| <= e by SEQ_1:10;
then |.(((lower_sum (((H . n) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k).| <= e by SEQ_1:7;
hence (abs ((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . k <= e by SEQ_1:12; :: thesis: verum

end;

A87: lower_sum (((H . n) || ['a,b']),T) is convergent by A7;
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 A54, SEQ_2:12;
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 A7;
then A88: 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, A19, A20, A13, INTEGRA4:8;
A89: (lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is convergent by A54, A87;
then |.((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))).| is convergent by SEQ_4:13;
then lim |.((lower_sum (((H . n) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))).| <= e by A86, PREPOWER:2;
hence |.((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e by A88, A89, SEQ_4:14; :: thesis: verum

end;

end;

A90: now :: thesis: for e1 being Real st 0 < e1 holds
|.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| < e1

let e1 be Real; :: thesis: ( 0 < e1 implies |.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| < e1 )
set e = e1 / 2;
assume A91: 0 < e1 ; :: thesis: |.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| < e1
then A92: 0 < e1 / 2 by XREAL_1:215;
then consider N1 being Element of NAT such that
A93: for n being Element of NAT st N1 <= n holds
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= (e1 / 2) / 2 by A46, XREAL_1:215;
consider N2 being Element of NAT such that
A94: for n being Element of NAT st N2 <= n holds
|.((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= (e1 / 2) / 2 by A83, A92, XREAL_1:215;
reconsider n = max (N1,N2) as Element of NAT ;
set K = upper_integral ((H . n) || ['a,b']);
set L = lower_integral ((H . n) || ['a,b']);
|.((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= (e1 / 2) / 2 by A94, XXREAL_0:25;
then A95: |.((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))).| <= (e1 / 2) / 2 by A7;
((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 A96: |.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= |.((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']))).| by COMPLEX1:57;
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= (e1 / 2) / 2 by A93, XXREAL_0:25;
then |.((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']))).| <= ((e1 / 2) / 2) + ((e1 / 2) / 2) by A95, XREAL_1:7;
then A97: |.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= e1 / 2 by A96, XXREAL_0:2;
e1 / 2 < e1 by A91, XREAL_1:216;
hence |.((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| < e1 by A97, XXREAL_0:2; :: thesis: verum

end;

A98: upper_integral ((lim (H,['a,b'])) || ['a,b']) = lower_integral ((lim (H,['a,b'])) || ['a,b']) by COMPLEX1:62, A90;
( (lim (H,['a,b'])) || ['a,b'] is upper_integrable & (lim (H,['a,b'])) || ['a,b'] is lower_integrable ) by A19, A20, A13, INTEGRA4:10;
then (lim (H,['a,b'])) || ['a,b'] is integrable by A98;
hence lim (H,['a,b']) is_integrable_on ['a,b'] ; :: thesis: ( rseq is convergent & lim rseq = integral ((lim (H,['a,b'])),a,b) )
A99: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - (integral ((lim (H,['a,b'])),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
|.((rseq . m) - (integral ((lim (H,['a,b'])),a,b))).| < p )
set e = p / 2;
assume A100: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((rseq . m) - (integral ((lim (H,['a,b'])),a,b))).| < p
then consider N being Element of NAT such that
A101: for n being Element of NAT st N <= n holds
|.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= p / 2 by A46, XREAL_1:215;
take N ; :: thesis: for m being Nat st N <= m holds
|.((rseq . m) - (integral ((lim (H,['a,b'])),a,b))).| < p
A102: p / 2 < p by A100, XREAL_1:216;

hereby :: thesis: verum

let n be Nat; :: thesis: ( N <= n implies |.((rseq . n) - (integral ((lim (H,['a,b'])),a,b))).| < p )
A103: n in NAT by ORDINAL1:def 12;
upper_integral ((H . n) || ['a,b']) = integral ((H . n) || ['a,b']) ;
then A104: upper_integral ((H . n) || ['a,b']) = rseq . n by A7, A103;
upper_integral ((lim (H,['a,b'])) || ['a,b']) = integral ((lim (H,['a,b'])),['a,b']) ;
then A105: upper_integral ((lim (H,['a,b'])) || ['a,b']) = integral ((lim (H,['a,b'])),a,b) by A1, INTEGRA5:def 4;
assume N <= n ; :: thesis: |.((rseq . n) - (integral ((lim (H,['a,b'])),a,b))).| < p
then |.((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))).| <= p / 2 by A101, A103;
hence |.((rseq . n) - (integral ((lim (H,['a,b'])),a,b))).| < p by A102, A104, A105, 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 A99, SEQ_2:def 7; :: thesis: verum