let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )
let f be Function of A,REAL ; :: thesis: for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )
let D be Division of A; :: thesis: for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )
let e be Real; :: thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i ) )
assume AS: ( f | A is bounded_above & 0 < e ) ; :: thesis: ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i )
defpred S1[ Nat, Element of REAL ] means ex r being Element of REAL st
( r in rng (f | (divset D,$1)) & $2 = r * (vol (divset D,$1)) & $2 <= (upper_volume f,D) . $1 & ((upper_volume f,D) . $1) - e < $2 );
A1: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of REAL st S1[k,x]
then P1: k in dom D by FINSEQ_1:def 3;
A10: ( rng (f | (divset D,k)) is bounded_above & not rng (f | (divset D,k)) is empty )
proof
rng f is bounded_above by AS, INTEGRA1:15;
hence rng (f | (divset D,k)) is bounded_above by RELAT_1:99, XXREAL_2:43; :: thesis: not rng (f | (divset D,k)) is empty
dom f = A by FUNCT_2:def 1;
then dom (f | (divset D,k)) = divset D,k by INTEGRA1:10, P1, RELAT_1:91;
hence not rng (f | (divset D,k)) is empty by RELAT_1:65; :: thesis: verum
end;
per cases ( vol (divset D,k) = 0 or vol (divset D,k) <> 0 ) ;
suppose C1: vol (divset D,k) = 0 ; :: thesis: ex x being Element of REAL st S1[k,x]
consider r being set such that
C11: r in rng (f | (divset D,k)) by A10, XBOOLE_0:def 1;
reconsider r = r as Element of REAL by C11;
reconsider x = r * (vol (divset D,k)) as Element of REAL ;
C12: (upper_volume f,D) . k = (upper_bound (rng (f | (divset D,k)))) * (vol (divset D,k)) by INTEGRA1:def 7, P1
.= 0 by C1 ;
then ((upper_volume f,D) . k) - e < x by AS, C1;
hence ex x being Element of REAL st S1[k,x] by C11, C12, C1; :: thesis: verum
end;
suppose C2: vol (divset D,k) <> 0 ; :: thesis: ex x being Element of REAL st S1[k,x]
then C21: 0 < vol (divset D,k) by INTEGRA1:11;
set e1 = e / (vol (divset D,k));
C22: 0 < e / (vol (divset D,k)) by C21, AS, XREAL_1:141;
set l = upper_bound (rng (f | (divset D,k)));
consider r being real number such that
C23: ( r in rng (f | (divset D,k)) & (upper_bound (rng (f | (divset D,k)))) - (e / (vol (divset D,k))) < r ) by C22, A10, SEQ_4:def 4;
C24: r <= upper_bound (rng (f | (divset D,k))) by A10, C23, SEQ_4:def 4;
reconsider x = r * (vol (divset D,k)) as Element of REAL ;
C25: (upper_volume f,D) . k = (upper_bound (rng (f | (divset D,k)))) * (vol (divset D,k)) by INTEGRA1:def 7, P1;
C26: x <= (upper_volume f,D) . k by C21, C24, C25, XREAL_1:66;
((upper_bound (rng (f | (divset D,k)))) - (e / (vol (divset D,k)))) * (vol (divset D,k)) < x by C21, C23, XREAL_1:70;
then ((upper_volume f,D) . k) - ((e / (vol (divset D,k))) * (vol (divset D,k))) < x by C25;
then ((upper_volume f,D) . k) - e < x by C2, XCMPLX_1:88;
hence ex x being Element of REAL st S1[k,x] by C23, C26; :: thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
B1: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from FINSEQ_1:sch 5(A1);
 B2: ( len p = len D & Seg (len D) = dom D ) by FINSEQ_1:def 3, B1;
now
let i be Nat; :: thesis: ( i in dom D implies ex r being Element of REAL st
( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) ) )
assume i in dom D ; :: thesis: ex r being Element of REAL st
( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) )
then i in Seg (len D) by FINSEQ_1:def 3;
then consider r being Element of REAL such that
C1: ( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) & p . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < p . i ) by B1;
take r = r; :: thesis: ( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) )
thus ( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) ) by C1; :: thesis: verum
end;
then reconsider p = p as middle_volume of f,D by defx0, B2;
now
let i be Nat; :: thesis: ( i in dom D implies ( p . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < p . i ) )
assume i in dom D ; :: thesis: ( p . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < p . i )
then i in Seg (len D) by FINSEQ_1:def 3;
then consider r being Element of REAL such that
C1: ( r in rng (f | (divset D,i)) & p . i = r * (vol (divset D,i)) & p . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < p . i ) by B1;
thus ( p . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < p . i ) by C1; :: thesis: verum
end;
hence ex F being middle_volume of f,D st
for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - e < F . i ) ; :: thesis: verum