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 S1[ 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 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 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 ;
then A5: not rng (f | (divset (D,k))) is empty by RELAT_1:42;
rng f is bounded_below by ;
then A6: rng (f | (divset (D,k))) is bounded_below by ;
per cases ( vol (divset (D,k)) = 0 or vol (divset (D,k)) <> 0 ) ;
suppose A7: vol (divset (D,k)) = 0 ; :: thesis: ex x being Element of REAL st S1[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
.= 0 by A7 ;
then x < ((lower_volume (f,D)) . k) + e by A2, A7;
hence ex x being Element of REAL st S1[k,x] by A7, A8, A9; :: thesis: verum
end;
suppose A10: vol (divset (D,k)) <> 0 ; :: thesis: ex x being Element of REAL st S1[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 ;
then 0 < e / (vol (divset (D,k))) by ;
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 ;
A14: (lower_volume (f,D)) . k = (lower_bound (rng (f | (divset (D,k))))) * (vol (divset (D,k))) by ;
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 ;
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 ;
lower_bound (rng (f | (divset (D,k)))) <= r by ;
then (lower_volume (f,D)) . k <= x by ;
hence ex x being Element of REAL st S1[k,x] by ; :: thesis: verum
end;
end;
end;
consider p being FinSequence of REAL such that
A16: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from
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))) )
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;
len p = len D by ;
then reconsider p = p as middle_volume of f,D by ;
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 )
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;
hence 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 ) ; :: thesis: verum