let A be non empty closed_interval Subset of REAL; :: thesis: for X being set

for f being PartFunc of REAL,REAL

for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let X be set ; :: thesis: for f being PartFunc of REAL,REAL

for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let f be PartFunc of REAL,REAL; :: thesis: for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let D be Division of A; :: thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is bounded implies ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) )

assume that

A1: A c= X and

A2: f is_differentiable_on X and

A3: (f `| X) | A is bounded ; :: thesis: ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

(len D) - 1 in NAT

deffunc H_{1}( Nat) -> Element of REAL = In ((f . (lower_bound (divset (D,($1 + 1))))),REAL);

deffunc H_{2}( Nat) -> Element of REAL = In (((f . (upper_bound (divset (D,$1)))) - (f . (lower_bound (divset (D,$1))))),REAL);

consider p being FinSequence of REAL such that

A4: ( len p = len D & ( for i being Nat st i in dom p holds

p . i = H_{2}(i) ) )
from FINSEQ_2:sch 1();

X c= dom f by A2, FDIFF_1:def 6;

then A5: A c= dom f by A1, XBOOLE_1:1;

A6: for k being Element of NAT st k in dom D holds

ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

A20: for i being Element of NAT st i in Seg k1 holds

upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

A29: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds

s2 . i = H_{1}(i) ) )
from FINSEQ_2:sch 1();

A30: for k being Element of NAT st k in dom D holds

rng (((f `| X) || A) | (divset (D,k))) is real-bounded_{3}( Nat) -> Element of REAL = In ((f . (upper_bound (divset (D,$1)))),REAL);

consider s1 being FinSequence of REAL such that

A39: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds

s1 . i = H_{3}(i) ) )
from FINSEQ_2:sch 1();

A40: dom s2 = Seg k1 by A29, FINSEQ_1:def 3;

reconsider flb = f . (lower_bound A), fub = f . (upper_bound A) as Element of REAL by XREAL_0:def 1;

( len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) & len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ) )

then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:74;

then A86: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:76;

A87: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;

A88: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;

for i being Nat st i in dom s1 holds

s1 . i = s2 . i

A91: for k being Element of NAT

for r being Real st k in dom D & r in divset (D,k) holds

diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k

(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k

for f being PartFunc of REAL,REAL

for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let X be set ; :: thesis: for f being PartFunc of REAL,REAL

for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let f be PartFunc of REAL,REAL; :: thesis: for D being Division of A st A c= X & f is_differentiable_on X & (f `| X) | A is bounded holds

( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

let D be Division of A; :: thesis: ( A c= X & f is_differentiable_on X & (f `| X) | A is bounded implies ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) ) )

assume that

A1: A c= X and

A2: f is_differentiable_on X and

A3: (f `| X) | A is bounded ; :: thesis: ( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )

(len D) - 1 in NAT

proof

then reconsider k1 = (len D) - 1 as Element of NAT ;
ex j being Nat st len D = 1 + j
by NAT_1:10, NAT_1:14;

hence (len D) - 1 in NAT by ORDINAL1:def 12; :: thesis: verum

end;hence (len D) - 1 in NAT by ORDINAL1:def 12; :: thesis: verum

deffunc H

deffunc H

consider p being FinSequence of REAL such that

A4: ( len p = len D & ( for i being Nat st i in dom p holds

p . i = H

X c= dom f by A2, FDIFF_1:def 6;

then A5: A c= dom f by A1, XBOOLE_1:1;

A6: for k being Element of NAT st k in dom D holds

ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

proof

A19:
dom p = Seg (len D)
by A4, FINSEQ_1:def 3;
let k be Element of NAT ; :: thesis: ( k in dom D implies ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) )

assume A7: k in dom D ; :: thesis: ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ; :: thesis: verum

end;( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) )

assume A7: k in dom D ; :: thesis: ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

now :: thesis: ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )end;

hence
ex r being Real st ( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

per cases
( lower_bound (divset (D,k)) = upper_bound (divset (D,k)) or lower_bound (divset (D,k)) <> upper_bound (divset (D,k)) )
;

end;

suppose A8:
lower_bound (divset (D,k)) = upper_bound (divset (D,k))
; :: thesis: ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

consider r being Real such that

A9: r = upper_bound (divset (D,k)) ;

A10: r in divset (D,k)

then vol (divset (D,k)) = 0 by INTEGRA1:def 5;

then (diff (f,r)) * (vol (divset (D,k))) = 0 ;

hence ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A8, A10; :: thesis: verum

end;A9: r = upper_bound (divset (D,k)) ;

A10: r in divset (D,k)

proof

(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) = 0
by A8;
ex a, b being Real st

( a <= b & a = lower_bound (divset (D,k)) & b = upper_bound (divset (D,k)) ) by SEQ_4:11;

hence r in divset (D,k) by A9, INTEGRA2:1; :: thesis: verum

end;( a <= b & a = lower_bound (divset (D,k)) & b = upper_bound (divset (D,k)) ) by SEQ_4:11;

hence r in divset (D,k) by A9, INTEGRA2:1; :: thesis: verum

then vol (divset (D,k)) = 0 by INTEGRA1:def 5;

then (diff (f,r)) * (vol (divset (D,k))) = 0 ;

hence ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A8, A10; :: thesis: verum

suppose A11:
lower_bound (divset (D,k)) <> upper_bound (divset (D,k))
; :: thesis: ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) )

ex r1, r2 being Real st

( r1 <= r2 & r1 = lower_bound (divset (D,k)) & r2 = upper_bound (divset (D,k)) ) by SEQ_4:11;

then A12: lower_bound (divset (D,k)) < upper_bound (divset (D,k)) by A11, XXREAL_0:1;

f | X is continuous by A2, FDIFF_1:25;

then f | A is continuous by A1, FCONT_1:16;

then A13: f | (divset (D,k)) is continuous by A7, FCONT_1:16, INTEGRA1:8;

A14: divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] by INTEGRA1:4;

then A15: ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= divset (D,k) by XXREAL_1:25;

A16: divset (D,k) c= A by A7, INTEGRA1:8;

then ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= A by A15, XBOOLE_1:1;

then f is_differentiable_on ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ by A1, A2, FDIFF_1:26, XBOOLE_1:1;

then consider r being Real such that

A17: r in ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ and

A18: diff (f,r) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) / ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) by A5, A16, A13, A12, A14, ROLLE:3, XBOOLE_1:1;

(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) > 0 by A12, XREAL_1:50;

then (diff (f,r)) * ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by A18, XCMPLX_1:87;

then (diff (f,r)) * (vol (divset (D,k))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by INTEGRA1:def 5;

hence ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A15, A17; :: thesis: verum

end;( r1 <= r2 & r1 = lower_bound (divset (D,k)) & r2 = upper_bound (divset (D,k)) ) by SEQ_4:11;

then A12: lower_bound (divset (D,k)) < upper_bound (divset (D,k)) by A11, XXREAL_0:1;

f | X is continuous by A2, FDIFF_1:25;

then f | A is continuous by A1, FCONT_1:16;

then A13: f | (divset (D,k)) is continuous by A7, FCONT_1:16, INTEGRA1:8;

A14: divset (D,k) = [.(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).] by INTEGRA1:4;

then A15: ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= divset (D,k) by XXREAL_1:25;

A16: divset (D,k) c= A by A7, INTEGRA1:8;

then ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ c= A by A15, XBOOLE_1:1;

then f is_differentiable_on ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ by A1, A2, FDIFF_1:26, XBOOLE_1:1;

then consider r being Real such that

A17: r in ].(lower_bound (divset (D,k))),(upper_bound (divset (D,k))).[ and

A18: diff (f,r) = ((f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k))))) / ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) by A5, A16, A13, A12, A14, ROLLE:3, XBOOLE_1:1;

(upper_bound (divset (D,k))) - (lower_bound (divset (D,k))) > 0 by A12, XREAL_1:50;

then (diff (f,r)) * ((upper_bound (divset (D,k))) - (lower_bound (divset (D,k)))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by A18, XCMPLX_1:87;

then (diff (f,r)) * (vol (divset (D,k))) = (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) by INTEGRA1:def 5;

hence ex r being Real st

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) by A15, A17; :: thesis: verum

( r in divset (D,k) & (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) ) ; :: thesis: verum

A20: for i being Element of NAT st i in Seg k1 holds

upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

proof

consider s2 being FinSequence of REAL such that
let i be Element of NAT ; :: thesis: ( i in Seg k1 implies upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) )

assume A21: i in Seg k1 ; :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

then i <= k1 by FINSEQ_1:1;

then A22: i + 1 <= k1 + 1 by XREAL_1:7;

1 <= i by A21, FINSEQ_1:1;

then 1 + 0 <= i + 1 by XREAL_1:7;

then i + 1 in Seg (len D) by A22, FINSEQ_1:1;

then A23: i + 1 in dom D by FINSEQ_1:def 3;

k1 + 1 = len D ;

then k1 <= len D by NAT_1:11;

then Seg k1 c= Seg (len D) by FINSEQ_1:5;

then i in Seg (len D) by A21;

then A24: i in dom D by FINSEQ_1:def 3;

A25: (i + 1) - 1 = i ;

end;assume A21: i in Seg k1 ; :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

then i <= k1 by FINSEQ_1:1;

then A22: i + 1 <= k1 + 1 by XREAL_1:7;

1 <= i by A21, FINSEQ_1:1;

then 1 + 0 <= i + 1 by XREAL_1:7;

then i + 1 in Seg (len D) by A22, FINSEQ_1:1;

then A23: i + 1 in dom D by FINSEQ_1:def 3;

k1 + 1 = len D ;

then k1 <= len D by NAT_1:11;

then Seg k1 c= Seg (len D) by FINSEQ_1:5;

then i in Seg (len D) by A21;

then A24: i in dom D by FINSEQ_1:def 3;

A25: (i + 1) - 1 = i ;

now :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))end;

hence
upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))
; :: thesis: verumper cases
( i = 1 or i <> 1 )
;

end;

suppose A26:
i = 1
; :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

then
upper_bound (divset (D,i)) = D . i
by A24, INTEGRA1:def 4;

hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A26, INTEGRA1:def 4; :: thesis: verum

end;hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A26, INTEGRA1:def 4; :: thesis: verum

suppose A27:
i <> 1
; :: thesis: upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1)))

i >= 1
by A21, FINSEQ_1:1;

then i + 1 >= 1 + 1 by XREAL_1:6;

then A28: i + 1 <> 1 ;

upper_bound (divset (D,i)) = D . i by A24, A27, INTEGRA1:def 4;

hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A28, INTEGRA1:def 4; :: thesis: verum

end;then i + 1 >= 1 + 1 by XREAL_1:6;

then A28: i + 1 <> 1 ;

upper_bound (divset (D,i)) = D . i by A24, A27, INTEGRA1:def 4;

hence upper_bound (divset (D,i)) = lower_bound (divset (D,(i + 1))) by A23, A25, A28, INTEGRA1:def 4; :: thesis: verum

A29: ( len s2 = k1 & ( for i being Nat st i in dom s2 holds

s2 . i = H

A30: for k being Element of NAT st k in dom D holds

rng (((f `| X) || A) | (divset (D,k))) is real-bounded

proof

deffunc H
dom (f `| X) = X
by A2, FDIFF_1:def 7;

then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:5;

let k be Element of NAT ; :: thesis: ( k in dom D implies rng (((f `| X) || A) | (divset (D,k))) is real-bounded )

assume k in dom D ; :: thesis: rng (((f `| X) || A) | (divset (D,k))) is real-bounded

consider r1 being Real such that

A31: for x being object st x in A /\ (dom (f `| X)) holds

(f `| X) . x <= r1 by A3, RFUNCT_1:70;

consider r2 being Real such that

A32: for x being object st x in A /\ (dom (f `| X)) holds

(f `| X) . x >= r2 by A3, RFUNCT_1:71;

A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61;

for x being object st x in A /\ (dom ((f `| X) || A)) holds

((f `| X) || A) . x >= r2

then A36: rng (((f `| X) || A) | (divset (D,k))) is bounded_below by INTEGRA4:19;

for x being object st x in A /\ (dom ((f `| X) || A)) holds

((f `| X) || A) . x <= r1

then rng (((f `| X) || A) | (divset (D,k))) is bounded_above by INTEGRA4:18;

hence rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A36; :: thesis: verum

end;then reconsider g = f `| X as PartFunc of X,REAL by RELSET_1:5;

let k be Element of NAT ; :: thesis: ( k in dom D implies rng (((f `| X) || A) | (divset (D,k))) is real-bounded )

assume k in dom D ; :: thesis: rng (((f `| X) || A) | (divset (D,k))) is real-bounded

consider r1 being Real such that

A31: for x being object st x in A /\ (dom (f `| X)) holds

(f `| X) . x <= r1 by A3, RFUNCT_1:70;

consider r2 being Real such that

A32: for x being object st x in A /\ (dom (f `| X)) holds

(f `| X) . x >= r2 by A3, RFUNCT_1:71;

A33: dom ((f `| X) | A) = (dom (f `| X)) /\ A by RELAT_1:61;

for x being object st x in A /\ (dom ((f `| X) || A)) holds

((f `| X) || A) . x >= r2

proof

then
((f `| X) || A) | A is bounded_below
by RFUNCT_1:71;
let x be object ; :: thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x >= r2 )

A34: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16

.= A /\ (dom (f `| X)) ;

reconsider y = g . x as Real ;

assume A35: x in A /\ (dom ((f `| X) || A)) ; :: thesis: ((f `| X) || A) . x >= r2

then y >= r2 by A32, A33, A34;

hence ((f `| X) || A) . x >= r2 by A33, A35, A34, FUNCT_1:47; :: thesis: verum

end;A34: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16

.= A /\ (dom (f `| X)) ;

reconsider y = g . x as Real ;

assume A35: x in A /\ (dom ((f `| X) || A)) ; :: thesis: ((f `| X) || A) . x >= r2

then y >= r2 by A32, A33, A34;

hence ((f `| X) || A) . x >= r2 by A33, A35, A34, FUNCT_1:47; :: thesis: verum

then A36: rng (((f `| X) || A) | (divset (D,k))) is bounded_below by INTEGRA4:19;

for x being object st x in A /\ (dom ((f `| X) || A)) holds

((f `| X) || A) . x <= r1

proof

then
((f `| X) || A) | A is bounded_above
by RFUNCT_1:70;
let x be object ; :: thesis: ( x in A /\ (dom ((f `| X) || A)) implies ((f `| X) || A) . x <= r1 )

A37: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16

.= A /\ (dom (f `| X)) ;

reconsider y = g . x as Real ;

assume A38: x in A /\ (dom ((f `| X) || A)) ; :: thesis: ((f `| X) || A) . x <= r1

then y <= r1 by A31, A33, A37;

hence ((f `| X) || A) . x <= r1 by A33, A38, A37, FUNCT_1:47; :: thesis: verum

end;A37: A /\ (A /\ (dom (f `| X))) = (A /\ A) /\ (dom (f `| X)) by XBOOLE_1:16

.= A /\ (dom (f `| X)) ;

reconsider y = g . x as Real ;

assume A38: x in A /\ (dom ((f `| X) || A)) ; :: thesis: ((f `| X) || A) . x <= r1

then y <= r1 by A31, A33, A37;

hence ((f `| X) || A) . x <= r1 by A33, A38, A37, FUNCT_1:47; :: thesis: verum

then rng (((f `| X) || A) | (divset (D,k))) is bounded_above by INTEGRA4:18;

hence rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A36; :: thesis: verum

consider s1 being FinSequence of REAL such that

A39: ( len s1 = k1 & ( for i being Nat st i in dom s1 holds

s1 . i = H

A40: dom s2 = Seg k1 by A29, FINSEQ_1:def 3;

reconsider flb = f . (lower_bound A), fub = f . (upper_bound A) as Element of REAL by XREAL_0:def 1;

( len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) & len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ) )

proof

then
Sum p = (Sum (s1 ^ <*(f . (upper_bound A))*>)) - (Sum (<*(f . (lower_bound A))*> ^ s2))
by INTEGRA1:22;
dom <*(f . (upper_bound A))*> = Seg 1
by FINSEQ_1:def 8;

then len <*(f . (upper_bound A))*> = 1 by FINSEQ_1:def 3;

then A41: len (s1 ^ <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:22;

dom <*(f . (lower_bound A))*> = Seg 1 by FINSEQ_1:def 8;

then len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:def 3;

hence A42: len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) by A29, A41, FINSEQ_1:22; :: thesis: ( len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ) )

thus len (s1 ^ <*(f . (upper_bound A))*>) = len p by A4, A41; :: thesis: for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

let i be Element of NAT ; :: thesis: ( i in dom (s1 ^ <*fub*>) implies p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) )

assume A43: i in dom (s1 ^ <*fub*>) ; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

then A44: (s1 ^ <*fub*>) /. i = (s1 ^ <*(f . (upper_bound A))*>) . i by PARTFUN1:def 6;

i in Seg (len (s1 ^ <*(f . (upper_bound A))*>)) by A43, FINSEQ_1:def 3;

then i in dom (<*(f . (lower_bound A))*> ^ s2) by A42, FINSEQ_1:def 3;

then A45: (<*flb*> ^ s2) /. i = (<*flb*> ^ s2) . i by PARTFUN1:def 6;

A46: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;

end;then len <*(f . (upper_bound A))*> = 1 by FINSEQ_1:def 3;

then A41: len (s1 ^ <*(f . (upper_bound A))*>) = k1 + 1 by A39, FINSEQ_1:22;

dom <*(f . (lower_bound A))*> = Seg 1 by FINSEQ_1:def 8;

then len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:def 3;

hence A42: len (s1 ^ <*(f . (upper_bound A))*>) = len (<*(f . (lower_bound A))*> ^ s2) by A29, A41, FINSEQ_1:22; :: thesis: ( len (s1 ^ <*(f . (upper_bound A))*>) = len p & ( for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) ) )

thus len (s1 ^ <*(f . (upper_bound A))*>) = len p by A4, A41; :: thesis: for i being Element of NAT st i in dom (s1 ^ <*fub*>) holds

p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

let i be Element of NAT ; :: thesis: ( i in dom (s1 ^ <*fub*>) implies p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) )

assume A43: i in dom (s1 ^ <*fub*>) ; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

then A44: (s1 ^ <*fub*>) /. i = (s1 ^ <*(f . (upper_bound A))*>) . i by PARTFUN1:def 6;

i in Seg (len (s1 ^ <*(f . (upper_bound A))*>)) by A43, FINSEQ_1:def 3;

then i in dom (<*(f . (lower_bound A))*> ^ s2) by A42, FINSEQ_1:def 3;

then A45: (<*flb*> ^ s2) /. i = (<*flb*> ^ s2) . i by PARTFUN1:def 6;

A46: ( len D = 1 or not len D is trivial ) by NAT_2:def 1;

now :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)end;

hence
p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)
; :: thesis: verumper cases
( len D = 1 or len D >= 2 )
by A46, NAT_2:29;

end;

suppose A47:
len D = 1
; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

then A48:
i in Seg 1
by A41, A43, FINSEQ_1:def 3;

then A49: i = 1 by FINSEQ_1:2, TARSKI:def 1;

s1 = {} by A39, A47;

then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:34;

then A50: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A44, A49, FINSEQ_1:def 8;

A51: i in dom D by A47, A48, FINSEQ_1:def 3;

s2 = {} by A29, A47;

then <*(f . (lower_bound A))*> ^ s2 = <*(f . (lower_bound A))*> by FINSEQ_1:34;

then A52: (<*flb*> ^ s2) /. i = f . (lower_bound A) by A45, A49, FINSEQ_1:def 8;

D . i = upper_bound A by A47, A49, INTEGRA1:def 2;

then A53: upper_bound (divset (D,i)) = upper_bound A by A49, A51, INTEGRA1:def 4;

p . i = H_{2}(i)
by A4, A19, A47, A48

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def 4; :: thesis: verum

end;then A49: i = 1 by FINSEQ_1:2, TARSKI:def 1;

s1 = {} by A39, A47;

then s1 ^ <*(f . (upper_bound A))*> = <*(f . (upper_bound A))*> by FINSEQ_1:34;

then A50: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A44, A49, FINSEQ_1:def 8;

A51: i in dom D by A47, A48, FINSEQ_1:def 3;

s2 = {} by A29, A47;

then <*(f . (lower_bound A))*> ^ s2 = <*(f . (lower_bound A))*> by FINSEQ_1:34;

then A52: (<*flb*> ^ s2) /. i = f . (lower_bound A) by A45, A49, FINSEQ_1:def 8;

D . i = upper_bound A by A47, A49, INTEGRA1:def 2;

then A53: upper_bound (divset (D,i)) = upper_bound A by A49, A51, INTEGRA1:def 4;

p . i = H

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A49, A51, A50, A52, A53, INTEGRA1:def 4; :: thesis: verum

suppose A54:
len D >= 2
; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

1 = 2 - 1
;

then A55: k1 >= 1 by A54, XREAL_1:9;

end;then A55: k1 >= 1 by A54, XREAL_1:9;

now :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)end;

hence
p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)
; :: thesis: verumper cases
( i = 1 or i = len D or ( i <> 1 & i <> len D ) )
;

end;

suppose A56:
i = 1
; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

then A57:
i in Seg 1
by FINSEQ_1:2, TARSKI:def 1;

then i in dom <*(f . (lower_bound A))*> by FINSEQ_1:def 8;

then (<*(f . (lower_bound A))*> ^ s2) . i = <*(f . (lower_bound A))*> . i by FINSEQ_1:def 7;

then A58: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound A) by A56, FINSEQ_1:def 8;

Seg 1 c= Seg k1 by A55, FINSEQ_1:5;

then i in Seg k1 by A57;

then A59: i in dom s1 by A39, FINSEQ_1:def 3;

then (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by FINSEQ_1:def 7

.= H_{3}(i)
by A39, A59
;

then A60: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) ;

A61: i in Seg 2 by A56, FINSEQ_1:2, TARSKI:def 2;

A62: Seg 2 c= Seg (len D) by A54, FINSEQ_1:5;

then i in Seg (len D) by A61;

then A63: i in dom D by FINSEQ_1:def 3;

p . i = H_{2}(i)
by A4, A19, A62, A61

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A44, A45, A56, A63, A60, A58, INTEGRA1:def 4; :: thesis: verum

end;then i in dom <*(f . (lower_bound A))*> by FINSEQ_1:def 8;

then (<*(f . (lower_bound A))*> ^ s2) . i = <*(f . (lower_bound A))*> . i by FINSEQ_1:def 7;

then A58: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound A) by A56, FINSEQ_1:def 8;

Seg 1 c= Seg k1 by A55, FINSEQ_1:5;

then i in Seg k1 by A57;

then A59: i in dom s1 by A39, FINSEQ_1:def 3;

then (s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by FINSEQ_1:def 7

.= H

then A60: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) ;

A61: i in Seg 2 by A56, FINSEQ_1:2, TARSKI:def 2;

A62: Seg 2 c= Seg (len D) by A54, FINSEQ_1:5;

then i in Seg (len D) by A61;

then A63: i in dom D by FINSEQ_1:def 3;

p . i = H

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A44, A45, A56, A63, A60, A58, INTEGRA1:def 4; :: thesis: verum

suppose A64:
i = len D
; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

then
i - (len s1) in Seg 1
by A39, FINSEQ_1:2, TARSKI:def 1;

then A65: i - (len s1) in dom <*(f . (upper_bound A))*> by FINSEQ_1:def 8;

i = (i - (len s1)) + (len s1) ;

then (s1 ^ <*(f . (upper_bound A))*>) . i = <*(f . (upper_bound A))*> . (i - (len s1)) by A65, FINSEQ_1:def 7;

then A66: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def 8;

A67: len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:40;

A68: i <> 1 by A54, A64;

i in Seg (len D) by A64, FINSEQ_1:3;

then A69: i in dom D by FINSEQ_1:def 3;

p . i = H_{2}(i)
by A4, A19, A64, FINSEQ_1:3

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

then p . i = (f . (upper_bound (divset (D,i)))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;

then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;

i - 1 <> 0 by A54, A64;

then A71: i - 1 in Seg k1 by A64, FINSEQ_1:3;

then reconsider i1 = i - 1 as Nat ;

A72: ( (len <*(f . (lower_bound A))*>) + (i - (len <*(f . (lower_bound A))*>)) = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) by A29, A67, FINSEQ_1:def 3, A71;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . i1 by FINSEQ_1:def 7, A67

.= H_{1}(i1)
by A29, A67, A72
;

then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) ;

then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def 4;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def 2; :: thesis: verum

end;then A65: i - (len s1) in dom <*(f . (upper_bound A))*> by FINSEQ_1:def 8;

i = (i - (len s1)) + (len s1) ;

then (s1 ^ <*(f . (upper_bound A))*>) . i = <*(f . (upper_bound A))*> . (i - (len s1)) by A65, FINSEQ_1:def 7;

then A66: (s1 ^ <*fub*>) /. i = f . (upper_bound A) by A39, A44, A64, FINSEQ_1:def 8;

A67: len <*(f . (lower_bound A))*> = 1 by FINSEQ_1:40;

A68: i <> 1 by A54, A64;

i in Seg (len D) by A64, FINSEQ_1:3;

then A69: i in dom D by FINSEQ_1:def 3;

p . i = H

.= (f . (upper_bound (divset (D,i)))) - (f . (lower_bound (divset (D,i)))) ;

then p . i = (f . (upper_bound (divset (D,i)))) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;

then A70: p . i = (f . (D . i)) - (f . (D . (i - 1))) by A69, A68, INTEGRA1:def 4;

i - 1 <> 0 by A54, A64;

then A71: i - 1 in Seg k1 by A64, FINSEQ_1:3;

then reconsider i1 = i - 1 as Nat ;

A72: ( (len <*(f . (lower_bound A))*>) + (i - (len <*(f . (lower_bound A))*>)) = i & i - (len <*(f . (lower_bound A))*>) in dom s2 ) by A29, A67, FINSEQ_1:def 3, A71;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . i1 by FINSEQ_1:def 7, A67

.= H

then (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) ;

then (<*(f . (lower_bound A))*> ^ s2) . i = f . (D . (i - 1)) by A69, A68, INTEGRA1:def 4;

hence p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A45, A64, A66, A70, INTEGRA1:def 2; :: thesis: verum

suppose A73:
( i <> 1 & i <> len D )
; :: thesis: p . i = ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i)

(len s1) + (len <*(f . (upper_bound A))*>) = k1 + 1
by A39, FINSEQ_1:39;

then A74: i in Seg (len D) by A43, FINSEQ_1:def 7;

A75: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

then i - (len <*(f . (lower_bound A))*>) <= len s2 by FINSEQ_1:1;

then A83: i <= (len <*(f . (lower_bound A))*>) + (len s2) by XREAL_1:20;

i >= 1 by A74, FINSEQ_1:1;

then reconsider i1 = i - 1 as Element of NAT by INT_1:5;

1 <= i - (len <*(f . (lower_bound A))*>) by A82, FINSEQ_1:1;

then (len <*(f . (lower_bound A))*>) + 1 <= i by XREAL_1:19;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by A83, FINSEQ_1:23;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:39

.= H_{1}(i1)
by A29, A40, A75
;

then A84: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) ;

(s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by A75, FINSEQ_1:def 7

.= H_{3}(i)
by A39, A75
;

then A85: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) ;

thus p . i = H_{2}(i)
by A4, A19, A74

.= ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A44, A45, A84, A85 ; :: thesis: verum

end;then A74: i in Seg (len D) by A43, FINSEQ_1:def 7;

A75: ( i in dom s1 & i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

proof

then A82:
i - (len <*(f . (lower_bound A))*>) in Seg (len s2)
by FINSEQ_1:def 3;
i <> 0
by A74, FINSEQ_1:1;

then not i is trivial by A73, NAT_2:def 1;

then i >= 1 + 1 by NAT_2:29;

then A76: i - 1 >= 1 by XREAL_1:19;

A77: 1 <= i by A74, FINSEQ_1:1;

i <= len D by A74, FINSEQ_1:1;

then A78: i < k1 + 1 by A73, XXREAL_0:1;

then A79: i <= k1 by NAT_1:13;

then i in Seg (len s1) by A39, A77, FINSEQ_1:1;

hence i in dom s1 by FINSEQ_1:def 3; :: thesis: ( i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

thus i in Seg k1 by A77, A79, FINSEQ_1:1; :: thesis: ( i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

i <= k1 by A78, NAT_1:13;

then i - 1 <= k1 - 1 by XREAL_1:9;

then A80: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7;

ex j being Nat st i = 1 + j by A77, NAT_1:10;

hence i - 1 in Seg k1 by A76, A80, FINSEQ_1:1; :: thesis: ( (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

then A81: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:39;

thus (i - 1) + 1 = i ; :: thesis: i - (len <*(f . (lower_bound A))*>) in dom s2

thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A81, FINSEQ_1:def 3; :: thesis: verum

end;then not i is trivial by A73, NAT_2:def 1;

then i >= 1 + 1 by NAT_2:29;

then A76: i - 1 >= 1 by XREAL_1:19;

A77: 1 <= i by A74, FINSEQ_1:1;

i <= len D by A74, FINSEQ_1:1;

then A78: i < k1 + 1 by A73, XXREAL_0:1;

then A79: i <= k1 by NAT_1:13;

then i in Seg (len s1) by A39, A77, FINSEQ_1:1;

hence i in dom s1 by FINSEQ_1:def 3; :: thesis: ( i in Seg k1 & i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

thus i in Seg k1 by A77, A79, FINSEQ_1:1; :: thesis: ( i - 1 in Seg k1 & (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

i <= k1 by A78, NAT_1:13;

then i - 1 <= k1 - 1 by XREAL_1:9;

then A80: (i - 1) + 0 <= (k1 - 1) + 1 by XREAL_1:7;

ex j being Nat st i = 1 + j by A77, NAT_1:10;

hence i - 1 in Seg k1 by A76, A80, FINSEQ_1:1; :: thesis: ( (i - 1) + 1 = i & i - (len <*(f . (lower_bound A))*>) in dom s2 )

then A81: i - (len <*(f . (lower_bound A))*>) in Seg (len s2) by A29, FINSEQ_1:39;

thus (i - 1) + 1 = i ; :: thesis: i - (len <*(f . (lower_bound A))*>) in dom s2

thus i - (len <*(f . (lower_bound A))*>) in dom s2 by A81, FINSEQ_1:def 3; :: thesis: verum

then i - (len <*(f . (lower_bound A))*>) <= len s2 by FINSEQ_1:1;

then A83: i <= (len <*(f . (lower_bound A))*>) + (len s2) by XREAL_1:20;

i >= 1 by A74, FINSEQ_1:1;

then reconsider i1 = i - 1 as Element of NAT by INT_1:5;

1 <= i - (len <*(f . (lower_bound A))*>) by A82, FINSEQ_1:1;

then (len <*(f . (lower_bound A))*>) + 1 <= i by XREAL_1:19;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - (len <*(f . (lower_bound A))*>)) by A83, FINSEQ_1:23;

then (<*(f . (lower_bound A))*> ^ s2) . i = s2 . (i - 1) by FINSEQ_1:39

.= H

then A84: (<*(f . (lower_bound A))*> ^ s2) . i = f . (lower_bound (divset (D,i))) ;

(s1 ^ <*(f . (upper_bound A))*>) . i = s1 . i by A75, FINSEQ_1:def 7

.= H

then A85: (s1 ^ <*(f . (upper_bound A))*>) . i = f . (upper_bound (divset (D,i))) ;

thus p . i = H

.= ((s1 ^ <*fub*>) /. i) - ((<*flb*> ^ s2) /. i) by A44, A45, A84, A85 ; :: thesis: verum

then Sum p = ((Sum s1) + (f . (upper_bound A))) - (Sum (<*(f . (lower_bound A))*> ^ s2)) by RVSUM_1:74;

then A86: Sum p = ((Sum s1) + (f . (upper_bound A))) - ((f . (lower_bound A)) + (Sum s2)) by RVSUM_1:76;

A87: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;

A88: dom s1 = Seg k1 by A39, FINSEQ_1:def 3;

for i being Nat st i in dom s1 holds

s1 . i = s2 . i

proof

then A90:
s1 = s2
by A39, A29, FINSEQ_2:9;
let i be Nat; :: thesis: ( i in dom s1 implies s1 . i = s2 . i )

assume A89: i in dom s1 ; :: thesis: s1 . i = s2 . i

then s1 . i = H_{3}(i)
by A39

.= f . (upper_bound (divset (D,i))) ;

then s1 . i = f . (lower_bound (divset (D,(i + 1)))) by A20, A87, A89

.= H_{1}(i)
;

hence s1 . i = s2 . i by A88, A29, A40, A89; :: thesis: verum

end;assume A89: i in dom s1 ; :: thesis: s1 . i = s2 . i

then s1 . i = H

.= f . (upper_bound (divset (D,i))) ;

then s1 . i = f . (lower_bound (divset (D,(i + 1)))) by A20, A87, A89

.= H

hence s1 . i = s2 . i by A88, A29, A40, A89; :: thesis: verum

A91: for k being Element of NAT

for r being Real st k in dom D & r in divset (D,k) holds

diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

proof

A98:
for k being Element of NAT st k in dom D holds
A92: dom ((f `| X) | A) =
(dom (f `| X)) /\ A
by RELAT_1:61

.= X /\ A by A2, FDIFF_1:def 7

.= A by A1, XBOOLE_1:28 ;

let k be Element of NAT ; :: thesis: for r being Real st k in dom D & r in divset (D,k) holds

diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

let r be Real; :: thesis: ( k in dom D & r in divset (D,k) implies diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) )

assume that

A93: k in dom D and

A94: r in divset (D,k) ; :: thesis: diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

A95: divset (D,k) c= A by A93, INTEGRA1:8;

then divset (D,k) c= X by A1, XBOOLE_1:1;

then (f `| X) . r = diff (f,r) by A2, A94, FDIFF_1:def 7;

then A96: diff (f,r) = ((f `| X) || A) . r by A94, A95, A92, FUNCT_1:47;

A97: dom (((f `| X) || A) | (divset (D,k))) = A /\ (divset (D,k)) by A92, RELAT_1:61

.= divset (D,k) by A93, INTEGRA1:8, XBOOLE_1:28 ;

then (((f `| X) || A) | (divset (D,k))) . r in rng (((f `| X) || A) | (divset (D,k))) by A94, FUNCT_1:def 3;

hence diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A94, A96, A97, FUNCT_1:47; :: thesis: verum

end;.= X /\ A by A2, FDIFF_1:def 7

.= A by A1, XBOOLE_1:28 ;

let k be Element of NAT ; :: thesis: for r being Real st k in dom D & r in divset (D,k) holds

diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

let r be Real; :: thesis: ( k in dom D & r in divset (D,k) implies diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) )

assume that

A93: k in dom D and

A94: r in divset (D,k) ; :: thesis: diff (f,r) in rng (((f `| X) || A) | (divset (D,k)))

A95: divset (D,k) c= A by A93, INTEGRA1:8;

then divset (D,k) c= X by A1, XBOOLE_1:1;

then (f `| X) . r = diff (f,r) by A2, A94, FDIFF_1:def 7;

then A96: diff (f,r) = ((f `| X) || A) . r by A94, A95, A92, FUNCT_1:47;

A97: dom (((f `| X) || A) | (divset (D,k))) = A /\ (divset (D,k)) by A92, RELAT_1:61

.= divset (D,k) by A93, INTEGRA1:8, XBOOLE_1:28 ;

then (((f `| X) || A) | (divset (D,k))) . r in rng (((f `| X) || A) | (divset (D,k))) by A94, FUNCT_1:def 3;

hence diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A94, A96, A97, FUNCT_1:47; :: thesis: verum

(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k

proof

A104:
(f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D)
let k be Element of NAT ; :: thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k )

A99: vol (divset (D,k)) >= 0 by INTEGRA1:9;

assume A100: k in dom D ; :: thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k

then consider r being Real such that

A101: r in divset (D,k) and

A102: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6;

A103: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A100;

diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A100, A101;

then diff (f,r) <= upper_bound (rng (((f `| X) || A) | (divset (D,k)))) by A103, SEQ_4:def 1;

then (diff (f,r)) * (vol (divset (D,k))) <= (upper_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) by A99, XREAL_1:64;

hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k by A100, A102, INTEGRA1:def 6; :: thesis: verum

end;A99: vol (divset (D,k)) >= 0 by INTEGRA1:9;

assume A100: k in dom D ; :: thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k

then consider r being Real such that

A101: r in divset (D,k) and

A102: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6;

A103: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A100;

diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A100, A101;

then diff (f,r) <= upper_bound (rng (((f `| X) || A) | (divset (D,k)))) by A103, SEQ_4:def 1;

then (diff (f,r)) * (vol (divset (D,k))) <= (upper_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) by A99, XREAL_1:64;

hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) <= (upper_volume (((f `| X) || A),D)) . k by A100, A102, INTEGRA1:def 6; :: thesis: verum

proof

A108:
for k being Element of NAT st k in dom D holds
len (upper_volume (((f `| X) || A),D)) = len D
by INTEGRA1:def 6;

then reconsider q = upper_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

A105: for k being Nat st k in Seg (len D) holds

p . k <= (upper_volume (((f `| X) || A),D)) . k

Sum p <= Sum q by A105, RVSUM_1:82;

hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 8; :: thesis: verum

end;then reconsider q = upper_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

A105: for k being Nat st k in Seg (len D) holds

p . k <= (upper_volume (((f `| X) || A),D)) . k

proof

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
let k be Nat; :: thesis: ( k in Seg (len D) implies p . k <= (upper_volume (((f `| X) || A),D)) . k )

assume A106: k in Seg (len D) ; :: thesis: p . k <= (upper_volume (((f `| X) || A),D)) . k

A107: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H_{2}(k)

.= p . k by A4, A19, A106 ;

k in dom D by FINSEQ_1:def 3, A106;

hence p . k <= (upper_volume (((f `| X) || A),D)) . k by A98, A107; :: thesis: verum

end;assume A106: k in Seg (len D) ; :: thesis: p . k <= (upper_volume (((f `| X) || A),D)) . k

A107: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H

.= p . k by A4, A19, A106 ;

k in dom D by FINSEQ_1:def 3, A106;

hence p . k <= (upper_volume (((f `| X) || A),D)) . k by A98, A107; :: thesis: verum

Sum p <= Sum q by A105, RVSUM_1:82;

hence (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 8; :: thesis: verum

(f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k

proof

(f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D)
let k be Element of NAT ; :: thesis: ( k in dom D implies (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k )

assume A109: k in dom D ; :: thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k

then A110: ( vol (divset (D,k)) >= 0 & (lower_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) = (lower_volume (((f `| X) || A),D)) . k ) by INTEGRA1:9, INTEGRA1:def 7;

A111: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A109;

consider r being Real such that

A112: r in divset (D,k) and

A113: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6, A109;

diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A109, A112;

then diff (f,r) >= lower_bound (rng (((f `| X) || A) | (divset (D,k)))) by A111, SEQ_4:def 2;

hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k by A113, A110, XREAL_1:64; :: thesis: verum

end;assume A109: k in dom D ; :: thesis: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k

then A110: ( vol (divset (D,k)) >= 0 & (lower_bound (rng (((f `| X) || A) | (divset (D,k))))) * (vol (divset (D,k))) = (lower_volume (((f `| X) || A),D)) . k ) by INTEGRA1:9, INTEGRA1:def 7;

A111: rng (((f `| X) || A) | (divset (D,k))) is real-bounded by A30, A109;

consider r being Real such that

A112: r in divset (D,k) and

A113: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = (diff (f,r)) * (vol (divset (D,k))) by A6, A109;

diff (f,r) in rng (((f `| X) || A) | (divset (D,k))) by A91, A109, A112;

then diff (f,r) >= lower_bound (rng (((f `| X) || A) | (divset (D,k)))) by A111, SEQ_4:def 2;

hence (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) >= (lower_volume (((f `| X) || A),D)) . k by A113, A110, XREAL_1:64; :: thesis: verum

proof

hence
( lower_sum (((f `| X) || A),D) <= (f . (upper_bound A)) - (f . (lower_bound A)) & (f . (upper_bound A)) - (f . (lower_bound A)) <= upper_sum (((f `| X) || A),D) )
by A104; :: thesis: verum
len (lower_volume (((f `| X) || A),D)) = len D
by INTEGRA1:def 7;

then reconsider q = lower_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

A114: for k being Nat st k in Seg (len D) holds

p . k >= (lower_volume (((f `| X) || A),D)) . k

Sum q <= Sum p by A114, RVSUM_1:82;

hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 9; :: thesis: verum

end;then reconsider q = lower_volume (((f `| X) || A),D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

A114: for k being Nat st k in Seg (len D) holds

p . k >= (lower_volume (((f `| X) || A),D)) . k

proof

reconsider p = p as Element of (len D) -tuples_on REAL by A4, FINSEQ_2:92;
let k be Nat; :: thesis: ( k in Seg (len D) implies p . k >= (lower_volume (((f `| X) || A),D)) . k )

assume A115: k in Seg (len D) ; :: thesis: p . k >= (lower_volume (((f `| X) || A),D)) . k

A116: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H_{2}(k)

.= p . k by A4, A19, A115 ;

k in dom D by FINSEQ_1:def 3, A115;

hence p . k >= (lower_volume (((f `| X) || A),D)) . k by A108, A116; :: thesis: verum

end;assume A115: k in Seg (len D) ; :: thesis: p . k >= (lower_volume (((f `| X) || A),D)) . k

A116: (f . (upper_bound (divset (D,k)))) - (f . (lower_bound (divset (D,k)))) = H

.= p . k by A4, A19, A115 ;

k in dom D by FINSEQ_1:def 3, A115;

hence p . k >= (lower_volume (((f `| X) || A),D)) . k by A108, A116; :: thesis: verum

Sum q <= Sum p by A114, RVSUM_1:82;

hence (f . (upper_bound A)) - (f . (lower_bound A)) >= lower_sum (((f `| X) || A),D) by A90, A86, INTEGRA1:def 9; :: thesis: verum