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 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 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 f

let f be Function of A,REAL; :: thesis: ( h is bounded & h is integrable & f = |.h.| & f is integrable implies |.().| <= integral f )
assume A1: ( h is bounded & h is integrable & f = |.h.| & f is integrable ) ; :: thesis:
then A2: f is bounded by Th14;
consider T being DivSequence of A such that
A3: ( delta T is convergent & lim () = 0 ) by INTEGRA4:11;
set S = the middle_volume_Sequence of h,T;
A4: dom f = dom h by ;
defpred S1[ 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 S1[k,p]
proof
let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S1[k,p]
defpred S2[ 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 S2[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S2[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 ;
( x in dom h & x in divset ((T . k),i) ) by ;
then reconsider x = x as Element of REAL ;
take x ; :: thesis: S2[i,x]
thus S2[i,x] by A8, A9; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A10: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S2[i,p . i] ) ) from take p ; :: thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by ;
hence ( p is Element of REAL * & S1[k,p] ) by ; :: thesis: verum
end;
consider F being sequence of () such that
A11: for x being Element of NAT holds S1[x,F . x] from defpred S2[ 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 S2[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Element of REAL * st S2[k,y]
defpred S3[ 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 S3[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S3[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S3[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 ;
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 ;
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 S3[i,x] by ; :: thesis: verum
end;
consider q being FinSequence of REAL such that
A19: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S3[i,q . i] ) ) from A20: len q = len (T . k) by ;
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))) )
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 ; :: thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by ;
q is Element of REAL * by FINSEQ_1:def 11;
hence ex y being Element of REAL * st S2[k,y] by ; :: thesis: verum
end;
consider Sf being sequence of () such that
A22: for x being Element of NAT holds S2[x,Sf . x] from
now :: thesis: for k being Element of NAT holds Sf . k is middle_volume of f,T . k
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;
then reconsider Sf = Sf as middle_volume_Sequence of f,T by INTEGR15:def 3;
A23: ( middle_sum (f,Sf) is convergent & lim (middle_sum (f,Sf)) = integral f ) by ;
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 ;
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;
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
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 ;
then A35: i in dom (T . k) by FINSEQ_1:def 3;
A36: i in dom (Sf . k) by ;
A37: (F . k) . i in dom (h | (divset ((T . k),i))) by ;
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 ;
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 ;
A40: ( the middle_volume_Sequence of h,T . k) /. i = ( the middle_volume_Sequence of h,T . k) . i by ;
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
.= (vol (divset ((T . k),i))) * |.z.| by ;
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
.= h /. ((F . k) . i) by ;
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
.= |.h.| /. ((F . k) . i) by
.= |.(h /. ((F . k) . i)).| by ;
hence |.(( the middle_volume_Sequence of h,T . k) /. i).| <= (Sf . k) /. i by ; :: thesis: verum
end;
then |.(middle_sum (h,( the middle_volume_Sequence of h,T . k))).| <= Sum (Sf . k) by Lm7, A28, A31, A32;
hence ||.((middle_sum (h, the middle_volume_Sequence of h,T)) . k).|| <= (middle_sum (f,Sf)) . k by ; :: thesis: verum
end;
A46: now :: thesis: for i being Nat holds ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| . i <= (middle_sum (f,Sf)) . iend;
||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| is convergent by ;
then lim ||.(middle_sum (h, the middle_volume_Sequence of h,T)).|| <= lim (middle_sum (f,Sf)) by ;
then ||.(lim (middle_sum (h, the middle_volume_Sequence of h,T))).|| <= lim (middle_sum (f,Sf)) by ;
hence |.().| <= integral f by ; :: thesis: verum