let A be non empty closed_interval Subset of REAL; :: thesis: for n being non zero Element of NAT

for h being Function of A,(REAL n)

for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let n be non zero Element of NAT ; :: thesis: for h being Function of A,(REAL n)

for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let h be Function of A,(REAL n); :: thesis: for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let f be Function of A,REAL; :: thesis: ( h is bounded & h is integrable & f = |.h.| & f is integrable implies |.(integral h).| <= integral f )

assume A1: ( h is bounded & h is integrable & f = |.h.| & f is integrable ) ; :: thesis: |.(integral h).| <= integral f

then A2: f is bounded by Th14;

consider T being DivSequence of A such that

A3: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;

set S = the middle_volume_Sequence of h,T;

A4: dom f = dom h by A1, NFCONT_4:def 2;

defpred S_{1}[ Element of NAT , set ] means ex p being FinSequence of REAL st

( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds

( p . i in dom (h | (divset ((T . $1),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . $1),i))) . (p . i) & ( the middle_volume_Sequence of h,T . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );

A5: for k being Element of NAT ex p being Element of REAL * st S_{1}[k,p]

A11: for x being Element of NAT holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A5);

defpred S_{2}[ Element of NAT , set ] means ex q being middle_volume of f,T . $1 st

( q = $2 & ( for i being Nat st i in dom (T . $1) holds

ex z being Element of REAL st

( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );

A12: for k being Element of NAT ex y being Element of REAL * st S_{2}[k,y]

A22: for x being Element of NAT holds S_{2}[x,Sf . x]
from FUNCT_2:sch 3(A12);

A23: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by A1, A2, A3, INTEGR15:9;

A24: ( middle_sum (h, the middle_volume_Sequence of h,T) is convergent & lim (middle_sum (h, the middle_volume_Sequence of h,T)) = integral h ) by A1, A3, INTEGR15:11;

A25: for k being Element of NAT holds ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k

then lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf)) by A46, A23, SEQ_2:18;

then ||.(lim (middle_sum (h, the middle_volume_Sequence of h,T))).|| <= lim (middle_sum (f,Sf)) by A24, LOPBAN_1:41;

hence |.(integral h).| <= integral f by A23, A1, A3, INTEGR15:11, REAL_NS1:1; :: thesis: verum

for h being Function of A,(REAL n)

for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let n be non zero Element of NAT ; :: thesis: for h being Function of A,(REAL n)

for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let h be Function of A,(REAL n); :: thesis: for f being Function of A,REAL st h is bounded & h is integrable & f = |.h.| & f is integrable holds

|.(integral h).| <= integral f

let f be Function of A,REAL; :: thesis: ( h is bounded & h is integrable & f = |.h.| & f is integrable implies |.(integral h).| <= integral f )

assume A1: ( h is bounded & h is integrable & f = |.h.| & f is integrable ) ; :: thesis: |.(integral h).| <= integral f

then A2: f is bounded by Th14;

consider T being DivSequence of A such that

A3: ( delta T is convergent & lim (delta T) = 0 ) by INTEGRA4:11;

set S = the middle_volume_Sequence of h,T;

A4: dom f = dom h by A1, NFCONT_4:def 2;

defpred S

( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds

( p . i in dom (h | (divset ((T . $1),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . $1),i))) . (p . i) & ( the middle_volume_Sequence of h,T . $1) . i = (vol (divset ((T . $1),i))) * z ) ) ) );

A5: for k being Element of NAT ex p being Element of REAL * st S

proof

consider F being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S_{1}[k,p]

defpred S_{2}[ Nat, set ] means ( $2 in dom (h | (divset ((T . k),$1))) & ex c being Element of REAL n st

( c = (h | (divset ((T . k),$1))) . $2 & ( the middle_volume_Sequence of h,T . k) . $1 = (vol (divset ((T . k),$1))) * c ) );

A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;

A7: for i being Nat st i in Seg (len (T . k)) holds

ex x being Element of REAL st S_{2}[i,x]

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{2}[i,p . i] ) )
from FINSEQ_1:sch 5(A7);

take p ; :: thesis: ( p is Element of REAL * & S_{1}[k,p] )

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S_{1}[k,p] )
by A10, A6, FINSEQ_1:def 11; :: thesis: verum

end;defpred S

( c = (h | (divset ((T . k),$1))) . $2 & ( the middle_volume_Sequence of h,T . k) . $1 = (vol (divset ((T . k),$1))) * c ) );

A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;

A7: for i being Nat st i in Seg (len (T . k)) holds

ex x being Element of REAL st S

proof

consider p being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{2}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{2}[i,x]

then i in dom (T . k) by FINSEQ_1:def 3;

then consider c being Element of REAL n such that

A8: ( c in rng (h | (divset ((T . k),i))) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR15:def 5;

consider x being object such that

A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def 3;

( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57;

then reconsider x = x as Element of REAL ;

take x ; :: thesis: S_{2}[i,x]

thus S_{2}[i,x]
by A8, A9; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

then i in dom (T . k) by FINSEQ_1:def 3;

then consider c being Element of REAL n such that

A8: ( c in rng (h | (divset ((T . k),i))) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR15:def 5;

consider x being object such that

A9: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def 3;

( x in dom h & x in divset ((T . k),i) ) by A9, RELAT_1:57;

then reconsider x = x as Element of REAL ;

take x ; :: thesis: S

thus S

A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

take p ; :: thesis: ( p is Element of REAL * & S

len p = len (T . k) by A10, FINSEQ_1:def 3;

hence ( p is Element of REAL * & S

A11: for x being Element of NAT holds S

defpred S

( q = $2 & ( for i being Nat st i in dom (T . $1) holds

ex z being Element of REAL st

( (F . $1) . i in dom (f | (divset ((T . $1),i))) & z = (f | (divset ((T . $1),i))) . ((F . $1) . i) & q . i = (vol (divset ((T . $1),i))) * z ) ) );

A12: for k being Element of NAT ex y being Element of REAL * st S

proof

consider Sf being sequence of (REAL *) such that
let k be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{2}[k,y]

defpred S_{3}[ Nat, set ] means ex c being Element of REAL st

( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );

A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;

A14: for i being Nat st i in Seg (len (T . k)) holds

ex x being Element of REAL st S_{3}[i,x]

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S_{3}[i,q . i] ) )
from FINSEQ_1:sch 5(A14);

A20: len q = len (T . k) by A19, FINSEQ_1:def 3;

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S_{2}[k,y]
by A13, A19; :: thesis: verum

end;defpred S

( (F . k) . $1 in dom (f | (divset ((T . k),$1))) & c = (f | (divset ((T . k),$1))) . ((F . k) . $1) & $2 = (vol (divset ((T . k),$1))) * c );

A13: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;

A14: for i being Nat st i in Seg (len (T . k)) holds

ex x being Element of REAL st S

proof

consider q being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S_{3}[i,x] )

assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S_{3}[i,x]

then A15: i in dom (T . k) by FINSEQ_1:def 3;

consider p being FinSequence of REAL such that

A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds

( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;

p . i in dom (h | (divset ((T . k),i))) by A15, A16;

then ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;

then A17: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A4, RELAT_1:57;

A18: (vol (divset ((T . k),i))) * ((f | (divset ((T . k),i))) . (p . i)) in REAL by XREAL_0:def 1;

(f | (divset ((T . k),i))) . (p . i) in REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S_{3}[i,x]
by A16, A17, A18; :: thesis: verum

end;assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S

then A15: i in dom (T . k) by FINSEQ_1:def 3;

consider p being FinSequence of REAL such that

A16: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds

( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;

p . i in dom (h | (divset ((T . k),i))) by A15, A16;

then ( p . i in dom h & p . i in divset ((T . k),i) ) by RELAT_1:57;

then A17: (F . k) . i in dom (f | (divset ((T . k),i))) by A16, A4, RELAT_1:57;

A18: (vol (divset ((T . k),i))) * ((f | (divset ((T . k),i))) . (p . i)) in REAL by XREAL_0:def 1;

(f | (divset ((T . k),i))) . (p . i) in REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S

A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds

S

A20: len q = len (T . k) by A19, FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (T . k) holds

ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) )

then reconsider q = q as middle_volume of f,T . k by A20, INTEGR15:def 1;ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) )

let i be Nat; :: thesis: ( i in dom (T . k) implies ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) )

assume i in dom (T . k) ; :: thesis: ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) )

then i in Seg (len (T . k)) by FINSEQ_1:def 3;

then consider c being Element of REAL such that

A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19;

thus ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) by A21, FUNCT_1:3; :: thesis: verum

end;( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) )

assume i in dom (T . k) ; :: thesis: ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) )

then i in Seg (len (T . k)) by FINSEQ_1:def 3;

then consider c being Element of REAL such that

A21: ( (F . k) . i in dom (f | (divset ((T . k),i))) & c = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * c ) by A19;

thus ex c being Element of REAL st

( c in rng (f | (divset ((T . k),i))) & q . i = c * (vol (divset ((T . k),i))) ) by A21, FUNCT_1:3; :: thesis: verum

q is Element of REAL * by FINSEQ_1:def 11;

hence ex y being Element of REAL * st S

A22: for x being Element of NAT holds S

now :: thesis: for k being Element of NAT holds Sf . k is middle_volume of f,T . k

then reconsider Sf = Sf as middle_volume_Sequence of f,T by INTEGR15:def 3;let k be Element of NAT ; :: thesis: Sf . k is middle_volume of f,T . k

ex q being middle_volume of f,T . k st

( q = Sf . k & ( for i being Nat st i in dom (T . k) holds

ex z being Element of REAL st

( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;

hence Sf . k is middle_volume of f,T . k ; :: thesis: verum

end;ex q being middle_volume of f,T . k st

( q = Sf . k & ( for i being Nat st i in dom (T . k) holds

ex z being Element of REAL st

( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;

hence Sf . k is middle_volume of f,T . k ; :: thesis: verum

A23: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by A1, A2, A3, INTEGR15:9;

A24: ( middle_sum (h, the middle_volume_Sequence of h,T) is convergent & lim (middle_sum (h, the middle_volume_Sequence of h,T)) = integral h ) by A1, A3, INTEGR15:11;

A25: for k being Element of NAT holds ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k

proof

let k be Element of NAT ; :: thesis: ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k

A26: (middle_sum (f,Sf)) . k = middle_sum (f,(Sf . k)) by INTEGR15:def 4

.= Sum (Sf . k) ;

A27: (middle_sum (h, the middle_volume_Sequence of h,T)) . k = middle_sum (h,( the middle_volume_Sequence of h,T . k)) by INTEGR15:def 8;

A28: for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * ( the middle_volume_Sequence of h,T . k) & (middle_sum (h,( the middle_volume_Sequence of h,T . k))) . i = Sum Pi ) by INTEGR15:def 6;

A29: ex p being FinSequence of REAL st

( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds

( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;

A30: ex q being middle_volume of f,T . k st

( q = Sf . k & ( for i being Nat st i in dom (T . k) holds

ex z being Element of REAL st

( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;

A31: len (Sf . k) = len (T . k) by INTEGR15:def 1;

A32: len ( the middle_volume_Sequence of h,T . k) = len (T . k) by INTEGR15:def 5;

hence ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k by A26, A27, REAL_NS1:1; :: thesis: verum

end;A26: (middle_sum (f,Sf)) . k = middle_sum (f,(Sf . k)) by INTEGR15:def 4

.= Sum (Sf . k) ;

A27: (middle_sum (h, the middle_volume_Sequence of h,T)) . k = middle_sum (h,( the middle_volume_Sequence of h,T . k)) by INTEGR15:def 8;

A28: for i being Element of NAT st i in Seg n holds

ex Pi being FinSequence of REAL st

( Pi = (proj (i,n)) * ( the middle_volume_Sequence of h,T . k) & (middle_sum (h,( the middle_volume_Sequence of h,T . k))) . i = Sum Pi ) by INTEGR15:def 6;

A29: ex p being FinSequence of REAL st

( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds

( p . i in dom (h | (divset ((T . k),i))) & ex z being Element of REAL n st

( z = (h | (divset ((T . k),i))) . (p . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) ) ) ) by A11;

A30: ex q being middle_volume of f,T . k st

( q = Sf . k & ( for i being Nat st i in dom (T . k) holds

ex z being Element of REAL st

( (F . k) . i in dom (f | (divset ((T . k),i))) & z = (f | (divset ((T . k),i))) . ((F . k) . i) & q . i = (vol (divset ((T . k),i))) * z ) ) ) by A22;

A31: len (Sf . k) = len (T . k) by INTEGR15:def 1;

A32: len ( the middle_volume_Sequence of h,T . k) = len (T . k) by INTEGR15:def 5;

now :: thesis: for i being Nat st i in dom ( the middle_volume_Sequence of h,T . k) holds

|.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i

then
|.(middle_sum (h,( the middle_volume_Sequence of h,T . k))).| <= Sum (Sf . k)
by Lm7, A28, A31, A32;|.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i

let i be Nat; :: thesis: ( i in dom ( the middle_volume_Sequence of h,T . k) implies |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i )

assume A33: i in dom ( the middle_volume_Sequence of h,T . k) ; :: thesis: |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i

then A34: i in Seg (len (T . k)) by A32, FINSEQ_1:def 3;

then A35: i in dom (T . k) by FINSEQ_1:def 3;

A36: i in dom (Sf . k) by A31, A34, FINSEQ_1:def 3;

A37: (F . k) . i in dom (h | (divset ((T . k),i))) by A35, A29;

consider z being Element of REAL n such that

A38: ( z = (h | (divset ((T . k),i))) . ((F . k) . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) by A29, A35;

consider w being Element of REAL such that

A39: ( (F . k) . i in dom (f | (divset ((T . k),i))) & w = (f | (divset ((T . k),i))) . ((F . k) . i) & (Sf . k) . i = (vol (divset ((T . k),i))) * w ) by A30, A35;

A40: ( the middle_volume_Sequence of h,T . k) /. i = ( the middle_volume_Sequence of h,T . k) . i by A33, PARTFUN1:def 6;

A41: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9;

A42: |.(( the middle_volume_Sequence of h,T . k) /. i).| = |.(vol (divset ((T . k),i))).| * |.z.| by A38, A40, EUCLID:11

.= (vol (divset ((T . k),i))) * |.z.| by A41, ABSVALUE:def 1 ;

A43: dom (h | (divset ((T . k),i))) c= dom h by RELAT_1:60;

A44: (h | (divset ((T . k),i))) . ((F . k) . i) = h . ((F . k) . i) by A37, FUNCT_1:47

.= h /. ((F . k) . i) by A43, A37, PARTFUN1:def 6 ;

A45: dom (f | (divset ((T . k),i))) c= dom f by RELAT_1:60;

(f | (divset ((T . k),i))) . ((F . k) . i) = f . ((F . k) . i) by A39, FUNCT_1:47

.= |.h.| /. ((F . k) . i) by A45, A1, A39, PARTFUN1:def 6

.= |.(h /. ((F . k) . i)).| by A45, A1, A39, NFCONT_4:def 2 ;

hence |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i by A42, A44, A39, A38, A36, PARTFUN1:def 6; :: thesis: verum

end;assume A33: i in dom ( the middle_volume_Sequence of h,T . k) ; :: thesis: |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i

then A34: i in Seg (len (T . k)) by A32, FINSEQ_1:def 3;

then A35: i in dom (T . k) by FINSEQ_1:def 3;

A36: i in dom (Sf . k) by A31, A34, FINSEQ_1:def 3;

A37: (F . k) . i in dom (h | (divset ((T . k),i))) by A35, A29;

consider z being Element of REAL n such that

A38: ( z = (h | (divset ((T . k),i))) . ((F . k) . i) & ( the middle_volume_Sequence of h,T . k) . i = (vol (divset ((T . k),i))) * z ) by A29, A35;

consider w being Element of REAL such that

A39: ( (F . k) . i in dom (f | (divset ((T . k),i))) & w = (f | (divset ((T . k),i))) . ((F . k) . i) & (Sf . k) . i = (vol (divset ((T . k),i))) * w ) by A30, A35;

A40: ( the middle_volume_Sequence of h,T . k) /. i = ( the middle_volume_Sequence of h,T . k) . i by A33, PARTFUN1:def 6;

A41: 0 <= vol (divset ((T . k),i)) by INTEGRA1:9;

A42: |.(( the middle_volume_Sequence of h,T . k) /. i).| = |.(vol (divset ((T . k),i))).| * |.z.| by A38, A40, EUCLID:11

.= (vol (divset ((T . k),i))) * |.z.| by A41, ABSVALUE:def 1 ;

A43: dom (h | (divset ((T . k),i))) c= dom h by RELAT_1:60;

A44: (h | (divset ((T . k),i))) . ((F . k) . i) = h . ((F . k) . i) by A37, FUNCT_1:47

.= h /. ((F . k) . i) by A43, A37, PARTFUN1:def 6 ;

A45: dom (f | (divset ((T . k),i))) c= dom f by RELAT_1:60;

(f | (divset ((T . k),i))) . ((F . k) . i) = f . ((F . k) . i) by A39, FUNCT_1:47

.= |.h.| /. ((F . k) . i) by A45, A1, A39, PARTFUN1:def 6

.= |.(h /. ((F . k) . i)).| by A45, A1, A39, NFCONT_4:def 2 ;

hence |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i by A42, A44, A39, A38, A36, PARTFUN1:def 6; :: thesis: verum

hence ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k by A26, A27, REAL_NS1:1; :: thesis: verum

A46: now :: thesis: for i being Nat holds ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i

||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| is convergent
by A1, A3, INTEGR15:11, NORMSP_1:23;let i be Nat; :: thesis: ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i

A47: i in NAT by ORDINAL1:def 12;

||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i = ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . i).|| by NORMSP_0:def 4;

hence ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i by A25, A47; :: thesis: verum

end;A47: i in NAT by ORDINAL1:def 12;

||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i = ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . i).|| by NORMSP_0:def 4;

hence ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . i by A25, A47; :: thesis: verum

then lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf)) by A46, A23, SEQ_2:18;

then ||.(lim (middle_sum (h, the middle_volume_Sequence of h,T))).|| <= lim (middle_sum (f,Sf)) by A24, LOPBAN_1:41;

hence |.(integral h).| <= integral f by A23, A1, A3, INTEGR15:11, REAL_NS1:1; :: thesis: verum