let A be non empty 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_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let f be Function of A,REAL; :: thesis: for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let D be Division of A; :: thesis: for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let e be Real; :: thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) )

assume that

A1: f | A is bounded_below and

A2: 0 < e ; :: thesis: ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

defpred S_{1}[ Nat, Real] means ex r being Element of REAL st

( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) & (lower_volume (f,D)) . $1 <= $2 & $2 < ((lower_volume (f,D)) . $1) + e );

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

ex x being Element of REAL st S_{1}[k,x]

A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds

S_{1}[k,p . k] ) )
from FINSEQ_1:sch 5(A3);

then reconsider p = p as middle_volume of f,D by A17, Def1;

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) ; :: thesis: verum

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let f be Function of A,REAL; :: thesis: for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let D be Division of A; :: thesis: for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

let e be Real; :: thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) )

assume that

A1: f | A is bounded_below and

A2: 0 < e ; :: thesis: ex F being middle_volume of f,D st

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e )

defpred S

( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) & (lower_volume (f,D)) . $1 <= $2 & $2 < ((lower_volume (f,D)) . $1) + e );

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

ex x being Element of REAL st S

proof

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

assume k in Seg (len D) ; :: thesis: ex x being Element of REAL st S_{1}[k,x]

then A4: k in dom D by FINSEQ_1:def 3;

dom f = A by FUNCT_2:def 1;

then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62;

then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42;

rng f is bounded_below by A1, INTEGRA1:11;

then A6: rng (f | (divset (D,k))) is bounded_below by RELAT_1:70, XXREAL_2:44;

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

then A4: k in dom D by FINSEQ_1:def 3;

dom f = A by FUNCT_2:def 1;

then dom (f | (divset (D,k))) = divset (D,k) by A4, INTEGRA1:8, RELAT_1:62;

then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42;

rng f is bounded_below by A1, INTEGRA1:11;

then A6: rng (f | (divset (D,k))) is bounded_below by RELAT_1:70, XXREAL_2:44;

per cases
( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 )
;

end;

suppose A7:
vol (divset (D,k)) = 0
; :: thesis: ex x being Element of REAL st S_{1}[k,x]

consider r being object such that

A8: r in rng (f | (divset (D,k))) by A5;

reconsider r = r as Element of REAL by A8;

reconsider x = r * (vol (divset (D,k))) as Element of REAL by XREAL_0:def 1;

A9: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def 7

.= 0 by A7 ;

then x < ((lower_volume (f,D)) . k) + e by A2, A7;

hence ex x being Element of REAL st S_{1}[k,x]
by A7, A8, A9; :: thesis: verum

end;A8: r in rng (f | (divset (D,k))) by A5;

reconsider r = r as Element of REAL by A8;

reconsider x = r * (vol (divset (D,k))) as Element of REAL by XREAL_0:def 1;

A9: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def 7

.= 0 by A7 ;

then x < ((lower_volume (f,D)) . k) + e by A2, A7;

hence ex x being Element of REAL st S

suppose A10:
vol (divset (D,k)) <> 0
; :: thesis: ex x being Element of REAL st S_{1}[k,x]

set l = lower_bound (rng (f | (divset (D,k))));

set e1 = e / (vol (divset (D,k)));

A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9;

then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139;

then consider r being Real such that

A12: r in rng (f | (divset (D,k))) and

A13: r < (lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k)))) by A6, A5, SEQ_4:def 2;

A14: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def 7;

reconsider x = r * (vol (divset (D,k))) as Element of REAL by XREAL_0:def 1;

x < ((lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))) * (vol (divset (D,k))) by A11, A13, XREAL_1:68;

then x < ((lower_volume (f,D)) . k) + ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) by A14;

then A15: x < ((lower_volume (f,D)) . k) + e by A10, XCMPLX_1:87;

lower_bound (rng (f | (divset (D,k)))) <= r by A6, A12, SEQ_4:def 2;

then (lower_volume (f,D)) . k <= x by A11, A14, XREAL_1:64;

hence ex x being Element of REAL st S_{1}[k,x]
by A12, A15; :: thesis: verum

end;set e1 = e / (vol (divset (D,k)));

A11: 0 < vol (divset (D,k)) by A10, INTEGRA1:9;

then 0 < e / (vol (divset (D,k))) by A2, XREAL_1:139;

then consider r being Real such that

A12: r in rng (f | (divset (D,k))) and

A13: r < (lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k)))) by A6, A5, SEQ_4:def 2;

A14: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by A4, INTEGRA1:def 7;

reconsider x = r * (vol (divset (D,k))) as Element of REAL by XREAL_0:def 1;

x < ((lower_bound (rng (f | (divset (D,k))))) + (e / (vol (divset (D,k))))) * (vol (divset (D,k))) by A11, A13, XREAL_1:68;

then x < ((lower_volume (f,D)) . k) + ((e / (vol (divset (D,k)))) * (vol (divset (D,k)))) by A14;

then A15: x < ((lower_volume (f,D)) . k) + e by A10, XCMPLX_1:87;

lower_bound (rng (f | (divset (D,k)))) <= r by A6, A12, SEQ_4:def 2;

then (lower_volume (f,D)) . k <= x by A11, A14, XREAL_1:64;

hence ex x being Element of REAL st S

A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds

S

A17: now :: thesis: for i being Nat st i in dom D holds

ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )

len p = len D
by A16, FINSEQ_1:def 3;ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) )

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

A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and

(lower_volume (f,D)) . i <= p . i and

p . i < ((lower_volume (f,D)) . i) + e by A16;

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 A18; :: thesis: verum

end;( 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

A18: ( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) ) and

(lower_volume (f,D)) . i <= p . i and

p . i < ((lower_volume (f,D)) . i) + e by A16;

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 A18; :: thesis: verum

then reconsider p = p as middle_volume of f,D by A17, Def1;

now :: thesis: for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )

hence
ex F being middle_volume of f,D st ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )

let i be Nat; :: thesis: ( i in dom D implies ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) )

assume i in dom D ; :: thesis: ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )

then i in Seg (len D) by FINSEQ_1:def 3;

then ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) by A16;

hence ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) ; :: thesis: verum

end;assume i in dom D ; :: thesis: ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e )

then i in Seg (len D) by FINSEQ_1:def 3;

then ex r being Element of REAL st

( r in rng (f | (divset (D,i))) & p . i = r * (vol (divset (D,i))) & (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) by A16;

hence ( (lower_volume (f,D)) . i <= p . i & p . i < ((lower_volume (f,D)) . i) + e ) ; :: thesis: verum

for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e ) ; :: thesis: verum