let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of A,REAL st f is bounded & A c= dom f & vol A > 0 holds

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

let f be PartFunc of A,REAL; :: thesis: ( f is bounded & A c= dom f & vol A > 0 implies ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) )

assume that

A1: f is bounded and

A2: A c= dom f and

A3: vol A > 0 ; :: thesis: ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

reconsider A1 = A as Element of Borel_Sets by MEASUR12:72;

defpred S_{1}[ Nat, PartFunc of REAL,ExtREAL] means ( A = dom $2 & $2 is_simple_func_in Borel_Sets & Integral (B-Meas,$2) = lower_sum (f,(EqDiv (A,(2 |^ $1)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= $2 . x & $2 . x <= f . x ) ) & ex K being Finite_Sep_Sequence of Borel_Sets st

( dom K = dom (EqDiv (A,(2 |^ $1))) & union (rng K) = A & ( for k being Nat st k in dom K holds

( ( len (EqDiv (A,(2 |^ $1))) = 1 implies K . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ $1))) <> 1 implies ( ( k = 1 implies K . k = [.(inf A),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).] ) ) ) ) ) & ( for x being Real st x in dom $2 holds

ex k being Nat st

( 1 <= k & k <= len K & x in K . k & $2 . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ $1))),k)))) ) ) ) );

A4: for n being Element of NAT ex g being Element of PFuncs (REAL,ExtREAL) st S_{1}[n,g]

A6: for n being Element of NAT holds S_{1}[n,F . n]
from FUNCT_2:sch 3(A4);

reconsider F = F as Functional_Sequence of REAL,ExtREAL ;

for n, m being Nat holds dom (F . n) = dom (F . m)

take F ; :: thesis: ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

A7: A = dom (F . 0) by A6;

A8: for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) )

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x )

A92: a <= b and

A93: A = [.a,b.] by MEASURE5:14;

reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;

A94: diameter A = b1 - a1 by A92, A93, MEASURE5:6;

B-Meas . A1 = diameter A by MEASUR12:71;

then A95: B-Meas . A1 < +infty by A94, XXREAL_0:4;

A96: for x being Element of REAL st x in A1 holds

F # x is convergent by A89;

A97: for n being Nat holds F . n is A1 -measurable by A8, MESFUNC2:34;

reconsider K = max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) as Real ;

A98: - |.(lower_bound (rng f)).| <= lower_bound (rng f) by ABSVALUE:4;

- K <= - |.(lower_bound (rng f)).| by XXREAL_0:25, XREAL_1:24;

then A99: - K <= lower_bound (rng f) by A98, XXREAL_0:2;

A100: upper_bound (rng f) <= |.(upper_bound (rng f)).| by ABSVALUE:4;

|.(upper_bound (rng f)).| <= K by XXREAL_0:25;

then A101: upper_bound (rng f) <= K by A100, XXREAL_0:2;

for n being Nat

for x being set st x in dom (F . 0) holds

|.((F . n) . x).| <= K

then ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) by A96, A97, A95, A7, MESFUN10:19;

hence ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) by A7, A8, A9, A89, A105, A96, A97, A95, MESFUN10:19; :: thesis: verum

ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

let f be PartFunc of A,REAL; :: thesis: ( f is bounded & A c= dom f & vol A > 0 implies ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) )

assume that

A1: f is bounded and

A2: A c= dom f and

A3: vol A > 0 ; :: thesis: ex F being with_the_same_dom Functional_Sequence of REAL,ExtREAL ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

reconsider A1 = A as Element of Borel_Sets by MEASUR12:72;

defpred S

( lower_bound (rng f) <= $2 . x & $2 . x <= f . x ) ) & ex K being Finite_Sep_Sequence of Borel_Sets st

( dom K = dom (EqDiv (A,(2 |^ $1))) & union (rng K) = A & ( for k being Nat st k in dom K holds

( ( len (EqDiv (A,(2 |^ $1))) = 1 implies K . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ $1))) <> 1 implies ( ( k = 1 implies K . k = [.(inf A),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ $1))) implies K . k = [.((EqDiv (A,(2 |^ $1))) . (k -' 1)),((EqDiv (A,(2 |^ $1))) . k).] ) ) ) ) ) & ( for x being Real st x in dom $2 holds

ex k being Nat st

( 1 <= k & k <= len K & x in K . k & $2 . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ $1))),k)))) ) ) ) );

A4: for n being Element of NAT ex g being Element of PFuncs (REAL,ExtREAL) st S

proof

consider F being Function of NAT,(PFuncs (REAL,ExtREAL)) such that
let n be Element of NAT ; :: thesis: ex g being Element of PFuncs (REAL,ExtREAL) st S_{1}[n,g]

consider K being Finite_Sep_Sequence of Borel_Sets , g being PartFunc of REAL,ExtREAL such that

A5: ( dom K = dom (EqDiv (A,(2 |^ n))) & union (rng K) = A & ( for k being Nat st k in dom K holds

( ( len (EqDiv (A,(2 |^ n))) = 1 implies K . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ n))) <> 1 implies ( ( k = 1 implies K . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ n))) implies K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ n))) implies K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len K & x in K . k & g . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= g . x & g . x <= f . x ) ) ) by A1, A2, Th19;

g is Element of PFuncs (REAL,ExtREAL) by PARTFUN1:45;

hence ex g being Element of PFuncs (REAL,ExtREAL) st S_{1}[n,g]
by A5; :: thesis: verum

end;consider K being Finite_Sep_Sequence of Borel_Sets , g being PartFunc of REAL,ExtREAL such that

A5: ( dom K = dom (EqDiv (A,(2 |^ n))) & union (rng K) = A & ( for k being Nat st k in dom K holds

( ( len (EqDiv (A,(2 |^ n))) = 1 implies K . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ n))) <> 1 implies ( ( k = 1 implies K . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ n))) implies K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ n))) implies K . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) & g is_simple_func_in Borel_Sets & ( for x being Real st x in dom g holds

ex k being Nat st

( 1 <= k & k <= len K & x in K . k & g . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) & dom g = A & Integral (B-Meas,g) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= g . x & g . x <= f . x ) ) ) by A1, A2, Th19;

g is Element of PFuncs (REAL,ExtREAL) by PARTFUN1:45;

hence ex g being Element of PFuncs (REAL,ExtREAL) st S

A6: for n being Element of NAT holds S

reconsider F = F as Functional_Sequence of REAL,ExtREAL ;

for n, m being Nat holds dom (F . n) = dom (F . m)

proof

then reconsider F = F as with_the_same_dom Functional_Sequence of REAL,ExtREAL by MESFUNC8:def 2;
let n, m be Nat; :: thesis: dom (F . n) = dom (F . m)

( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;

then ( S_{1}[n,F . n] & S_{1}[m,F . m] )
by A6;

hence dom (F . n) = dom (F . m) ; :: thesis: verum

end;( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;

then ( S

hence dom (F . n) = dom (F . m) ; :: thesis: verum

take F ; :: thesis: ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) )

A7: A = dom (F . 0) by A6;

A8: for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) )

proof

A9:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: ( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) )

n is Element of NAT by ORDINAL1:def 12;

hence ( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) by A6; :: thesis: verum

end;( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) )

n is Element of NAT by ORDINAL1:def 12;

hence ( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) by A6; :: thesis: verum

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x

proof

A89:
for x being Element of REAL st x in A holds
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x )

assume A10: n <= m ; :: thesis: for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x

A11: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;

let x be Element of REAL ; :: thesis: ( x in A implies (F . n) . x <= (F . m) . x )

assume A12: x in A ; :: thesis: (F . n) . x <= (F . m) . x

consider Kn being Finite_Sep_Sequence of Borel_Sets such that

A13: ( dom Kn = dom (EqDiv (A,(2 |^ n))) & union (rng Kn) = A & ( for k being Nat st k in dom Kn holds

( ( len (EqDiv (A,(2 |^ n))) = 1 implies Kn . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ n))) <> 1 implies ( ( k = 1 implies Kn . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ n))) implies Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ n))) implies Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) & ( for x being Real st x in dom (F . n) holds

ex k being Nat st

( 1 <= k & k <= len Kn & x in Kn . k & (F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) ) by A6, A11;

consider Km being Finite_Sep_Sequence of Borel_Sets such that

A14: ( dom Km = dom (EqDiv (A,(2 |^ m))) & union (rng Km) = A & ( for k being Nat st k in dom Km holds

( ( len (EqDiv (A,(2 |^ m))) = 1 implies Km . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ m))) <> 1 implies ( ( k = 1 implies Km . k = [.(inf A),((EqDiv (A,(2 |^ m))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ m))) implies Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ m))) implies Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).] ) ) ) ) ) & ( for x being Real st x in dom (F . m) holds

ex k being Nat st

( 1 <= k & k <= len Km & x in Km . k & (F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k)))) ) ) ) by A6, A11;

A15: ( len (EqDiv (A,(2 |^ n))) = len Kn & len (EqDiv (A,(2 |^ m))) = len Km ) by A13, A14, FINSEQ_3:29;

x in dom (F . n) by A6, A11, A12;

then consider k1 being Nat such that

A16: ( 1 <= k1 & k1 <= len Kn & x in Kn . k1 & (F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k1)))) ) by A13;

x in dom (F . m) by A6, A11, A12;

then consider k2 being Nat such that

A17: ( 1 <= k2 & k2 <= len Km & x in Km . k2 & (F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k2)))) ) by A14;

A18: ( k1 - 1 = k1 -' 1 & k2 - 1 = k2 -' 1 ) by A16, A17, XREAL_1:48, XREAL_0:def 2;

A19: ( k1 in dom Kn & k2 in dom Km ) by A16, A17, FINSEQ_3:25;

then divset ((EqDiv (A,(2 |^ n))),k1) c= A by A13, INTEGRA1:8;

then A20: divset ((EqDiv (A,(2 |^ n))),k1) c= dom f by A2;

f = f | (dom f) ;

then f | (divset ((EqDiv (A,(2 |^ n))),k1)) is bounded by A1, A20, RFUNCT_1:74;

then A21: rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is real-bounded by INTEGRA1:15;

divset ((EqDiv (A,(2 |^ m))),k2) c= A by A14, A19, INTEGRA1:8;

then divset ((EqDiv (A,(2 |^ m))),k2) c= dom f by A2;

then dom (f | (divset ((EqDiv (A,(2 |^ m))),k2))) = divset ((EqDiv (A,(2 |^ m))),k2) by RELAT_1:62;

then A22: rng (f | (divset ((EqDiv (A,(2 |^ m))),k2))) <> {} by RELAT_1:42;

A23: ( 2 |^ n > 0 & 2 |^ m > 0 ) by NEWTON:83;

then A24: ( EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n & EqDiv (A,(2 |^ m)) divide_into_equal 2 |^ m ) by A3, Def1;

then A25: ( len (EqDiv (A,(2 |^ n))) = 2 |^ n & len (EqDiv (A,(2 |^ m))) = 2 |^ m ) by INTEGRA4:def 1;

then A26: ( (EqDiv (A,(2 |^ n))) . k1 = (lower_bound A) + (((vol A) / (2 |^ n)) * k1) & (EqDiv (A,(2 |^ m))) . k2 = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A24, A13, A14, A16, A17, FINSEQ_3:25, INTEGRA4:def 1;

A27: m - n >= 0 by A10, XREAL_1:48;

A28: m -' n = m - n by A10, XREAL_1:48, XREAL_0:def 2;

( 2 |^ n >= 1 & 2 |^ m >= 1 ) by A23, NAT_1:14;

then A29: ( (2 |^ n) -' 1 = (2 |^ n) - 1 & (2 |^ m) -' 1 = (2 |^ m) - 1 ) by XREAL_0:def 2, XREAL_1:48;

A30: (2 |^ (m -' n)) * ((2 |^ n) - 1) = ((2 |^ (m -' n)) * (2 |^ n)) - (2 |^ (m -' n))

.= (2 |^ ((m -' n) + n)) - (2 |^ (m -' n)) by NEWTON:8

.= (2 |^ m) - (2 |^ (m -' n)) by A27, NAT_D:72 ;

A31: 2 |^ (m -' n) <= 2 |^ m by PREPOWER:93, NAT_D:35;

( (2 |^ n) * (2 |^ (m -' n)) = 2 |^ m & (2 |^ n) * ((2 |^ (m -' n)) -' 1) < 2 |^ m ) by A10, Lm5;

then A37: 2 |^ n = (2 |^ m) / (2 |^ (m -' n)) by A36, XCMPLX_1:89;

A38: (vol A) / (2 |^ n) = ((vol A) / (2 |^ m)) * (2 |^ (m -' n)) by A37, XCMPLX_1:81;

then A39: ( ((vol A) / (2 |^ n)) * k1 = ((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) & ((vol A) / (2 |^ n)) * (k1 -' 1) = ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) ) ;

divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

hence (F . n) . x <= (F . m) . x by A16, A17, A21, A22, SEQ_4:47, RELAT_1:11; :: thesis: verum

end;(F . n) . x <= (F . m) . x )

assume A10: n <= m ; :: thesis: for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x

A11: ( n is Element of NAT & m is Element of NAT ) by ORDINAL1:def 12;

let x be Element of REAL ; :: thesis: ( x in A implies (F . n) . x <= (F . m) . x )

assume A12: x in A ; :: thesis: (F . n) . x <= (F . m) . x

consider Kn being Finite_Sep_Sequence of Borel_Sets such that

A13: ( dom Kn = dom (EqDiv (A,(2 |^ n))) & union (rng Kn) = A & ( for k being Nat st k in dom Kn holds

( ( len (EqDiv (A,(2 |^ n))) = 1 implies Kn . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ n))) <> 1 implies ( ( k = 1 implies Kn . k = [.(inf A),((EqDiv (A,(2 |^ n))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ n))) implies Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ n))) implies Kn . k = [.((EqDiv (A,(2 |^ n))) . (k -' 1)),((EqDiv (A,(2 |^ n))) . k).] ) ) ) ) ) & ( for x being Real st x in dom (F . n) holds

ex k being Nat st

( 1 <= k & k <= len Kn & x in Kn . k & (F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) ) by A6, A11;

consider Km being Finite_Sep_Sequence of Borel_Sets such that

A14: ( dom Km = dom (EqDiv (A,(2 |^ m))) & union (rng Km) = A & ( for k being Nat st k in dom Km holds

( ( len (EqDiv (A,(2 |^ m))) = 1 implies Km . k = [.(inf A),(sup A).] ) & ( len (EqDiv (A,(2 |^ m))) <> 1 implies ( ( k = 1 implies Km . k = [.(inf A),((EqDiv (A,(2 |^ m))) . k).[ ) & ( 1 < k & k < len (EqDiv (A,(2 |^ m))) implies Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).[ ) & ( k = len (EqDiv (A,(2 |^ m))) implies Km . k = [.((EqDiv (A,(2 |^ m))) . (k -' 1)),((EqDiv (A,(2 |^ m))) . k).] ) ) ) ) ) & ( for x being Real st x in dom (F . m) holds

ex k being Nat st

( 1 <= k & k <= len Km & x in Km . k & (F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k)))) ) ) ) by A6, A11;

A15: ( len (EqDiv (A,(2 |^ n))) = len Kn & len (EqDiv (A,(2 |^ m))) = len Km ) by A13, A14, FINSEQ_3:29;

x in dom (F . n) by A6, A11, A12;

then consider k1 being Nat such that

A16: ( 1 <= k1 & k1 <= len Kn & x in Kn . k1 & (F . n) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k1)))) ) by A13;

x in dom (F . m) by A6, A11, A12;

then consider k2 being Nat such that

A17: ( 1 <= k2 & k2 <= len Km & x in Km . k2 & (F . m) . x = lower_bound (rng (f | (divset ((EqDiv (A,(2 |^ m))),k2)))) ) by A14;

A18: ( k1 - 1 = k1 -' 1 & k2 - 1 = k2 -' 1 ) by A16, A17, XREAL_1:48, XREAL_0:def 2;

A19: ( k1 in dom Kn & k2 in dom Km ) by A16, A17, FINSEQ_3:25;

then divset ((EqDiv (A,(2 |^ n))),k1) c= A by A13, INTEGRA1:8;

then A20: divset ((EqDiv (A,(2 |^ n))),k1) c= dom f by A2;

f = f | (dom f) ;

then f | (divset ((EqDiv (A,(2 |^ n))),k1)) is bounded by A1, A20, RFUNCT_1:74;

then A21: rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is real-bounded by INTEGRA1:15;

divset ((EqDiv (A,(2 |^ m))),k2) c= A by A14, A19, INTEGRA1:8;

then divset ((EqDiv (A,(2 |^ m))),k2) c= dom f by A2;

then dom (f | (divset ((EqDiv (A,(2 |^ m))),k2))) = divset ((EqDiv (A,(2 |^ m))),k2) by RELAT_1:62;

then A22: rng (f | (divset ((EqDiv (A,(2 |^ m))),k2))) <> {} by RELAT_1:42;

A23: ( 2 |^ n > 0 & 2 |^ m > 0 ) by NEWTON:83;

then A24: ( EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n & EqDiv (A,(2 |^ m)) divide_into_equal 2 |^ m ) by A3, Def1;

then A25: ( len (EqDiv (A,(2 |^ n))) = 2 |^ n & len (EqDiv (A,(2 |^ m))) = 2 |^ m ) by INTEGRA4:def 1;

then A26: ( (EqDiv (A,(2 |^ n))) . k1 = (lower_bound A) + (((vol A) / (2 |^ n)) * k1) & (EqDiv (A,(2 |^ m))) . k2 = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A24, A13, A14, A16, A17, FINSEQ_3:25, INTEGRA4:def 1;

A27: m - n >= 0 by A10, XREAL_1:48;

A28: m -' n = m - n by A10, XREAL_1:48, XREAL_0:def 2;

( 2 |^ n >= 1 & 2 |^ m >= 1 ) by A23, NAT_1:14;

then A29: ( (2 |^ n) -' 1 = (2 |^ n) - 1 & (2 |^ m) -' 1 = (2 |^ m) - 1 ) by XREAL_0:def 2, XREAL_1:48;

A30: (2 |^ (m -' n)) * ((2 |^ n) - 1) = ((2 |^ (m -' n)) * (2 |^ n)) - (2 |^ (m -' n))

.= (2 |^ ((m -' n) + n)) - (2 |^ (m -' n)) by NEWTON:8

.= (2 |^ m) - (2 |^ (m -' n)) by A27, NAT_D:72 ;

A31: 2 |^ (m -' n) <= 2 |^ m by PREPOWER:93, NAT_D:35;

A32: now :: thesis: ( 1 <> k1 implies (EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) )

assume
1 <> k1
; :: thesis: (EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1))

then 1 < k1 by A16, XXREAL_0:1;

then A33: k1 -' 1 >= 1 by NAT_1:14, NAT_D:36;

k1 -' 1 <= k1 by NAT_D:35;

then k1 -' 1 <= len Kn by A16, XXREAL_0:2;

hence (EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A24, A25, A33, A13, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum

end;then 1 < k1 by A16, XXREAL_0:1;

then A33: k1 -' 1 >= 1 by NAT_1:14, NAT_D:36;

k1 -' 1 <= k1 by NAT_D:35;

then k1 -' 1 <= len Kn by A16, XXREAL_0:2;

hence (EqDiv (A,(2 |^ n))) . (k1 -' 1) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A24, A25, A33, A13, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum

A34: now :: thesis: ( 1 <> k2 implies (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) )

A36:
2 |^ (m -' n) > 0
by NEWTON:83;assume
1 <> k2
; :: thesis: (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1))

then 1 < k2 by A17, XXREAL_0:1;

then A35: k2 -' 1 >= 1 by NAT_1:14, NAT_D:36;

k2 -' 1 <= k2 by NAT_D:35;

then k2 -' 1 <= len Km by A17, XXREAL_0:2;

hence (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A24, A25, A35, A14, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum

end;then 1 < k2 by A17, XXREAL_0:1;

then A35: k2 -' 1 >= 1 by NAT_1:14, NAT_D:36;

k2 -' 1 <= k2 by NAT_D:35;

then k2 -' 1 <= len Km by A17, XXREAL_0:2;

hence (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A24, A25, A35, A14, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum

( (2 |^ n) * (2 |^ (m -' n)) = 2 |^ m & (2 |^ n) * ((2 |^ (m -' n)) -' 1) < 2 |^ m ) by A10, Lm5;

then A37: 2 |^ n = (2 |^ m) / (2 |^ (m -' n)) by A36, XCMPLX_1:89;

A38: (vol A) / (2 |^ n) = ((vol A) / (2 |^ m)) * (2 |^ (m -' n)) by A37, XCMPLX_1:81;

then A39: ( ((vol A) / (2 |^ n)) * k1 = ((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) & ((vol A) / (2 |^ n)) * (k1 -' 1) = ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) ) ;

divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

proof
end;

then
f | (divset ((EqDiv (A,(2 |^ m))),k2)) c= f | (divset ((EqDiv (A,(2 |^ n))),k1))
by RELAT_1:75;per cases
( len (EqDiv (A,(2 |^ m))) = 1 or len (EqDiv (A,(2 |^ m))) <> 1 )
;

end;

suppose A40:
len (EqDiv (A,(2 |^ m))) = 1
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then A41:
2 |^ n <= 1
by A10, A25, PREPOWER:93;

len (EqDiv (A,(2 |^ n))) = 1 by A25, A10, A40, PREPOWER:93, NAT_1:25;

then len Kn = 1 by A13, FINSEQ_3:29;

then k1 = 1 by A16, XXREAL_0:1;

then divset ((EqDiv (A,(2 |^ n))),k1) = A by A3, A41, A25, Lm4, NAT_1:25;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A19, A14, INTEGRA1:8; :: thesis: verum

end;len (EqDiv (A,(2 |^ n))) = 1 by A25, A10, A40, PREPOWER:93, NAT_1:25;

then len Kn = 1 by A13, FINSEQ_3:29;

then k1 = 1 by A16, XXREAL_0:1;

then divset ((EqDiv (A,(2 |^ n))),k1) = A by A3, A41, A25, Lm4, NAT_1:25;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A19, A14, INTEGRA1:8; :: thesis: verum

suppose A42:
len (EqDiv (A,(2 |^ m))) <> 1
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

end;

per cases
( len (EqDiv (A,(2 |^ n))) = 1 or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = 1 ) or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = len (EqDiv (A,(2 |^ m))) ) or ( len (EqDiv (A,(2 |^ n))) <> 1 & k2 <> 1 & k2 <> len (EqDiv (A,(2 |^ m))) ) )
;

end;

suppose A43:
len (EqDiv (A,(2 |^ n))) = 1
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
len Kn = 1
by A13, FINSEQ_3:29;

then k1 = 1 by A16, XXREAL_0:1;

then divset ((EqDiv (A,(2 |^ n))),k1) = A by A3, A43, Lm4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A19, A14, INTEGRA1:8; :: thesis: verum

end;then k1 = 1 by A16, XXREAL_0:1;

then divset ((EqDiv (A,(2 |^ n))),k1) = A by A3, A43, Lm4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A19, A14, INTEGRA1:8; :: thesis: verum

suppose A44:
( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = 1 )
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
Km . k2 = [.(inf A),((EqDiv (A,(2 |^ m))) . k2).[
by A14, A19, A42;

then A45: ( inf A <= x & x < (EqDiv (A,(2 |^ m))) . k2 ) by A17, XXREAL_1:3;

2 |^ n divides 2 |^ m by A10, NEWTON:89;

then 2 |^ n <= 2 |^ m by A23, NAT_D:7;

then A46: ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * 1 by A3, A23, XREAL_1:118;

((vol A) / (2 |^ n)) * 1 <= ((vol A) / (2 |^ n)) * k1 by A16, A3, XREAL_1:64;

then ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * k1 by A46, XXREAL_0:2;

then A47: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A44, A26, XREAL_1:7;

then A50: divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound A),((EqDiv (A,(2 |^ n))) . k1).] by INTEGRA1:4;

( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A44, A14, A19, INTEGRA1:def 4;

then divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound A),((EqDiv (A,(2 |^ m))) . k2).] by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A47, A50, XXREAL_1:34; :: thesis: verum

end;then A45: ( inf A <= x & x < (EqDiv (A,(2 |^ m))) . k2 ) by A17, XXREAL_1:3;

2 |^ n divides 2 |^ m by A10, NEWTON:89;

then 2 |^ n <= 2 |^ m by A23, NAT_D:7;

then A46: ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * 1 by A3, A23, XREAL_1:118;

((vol A) / (2 |^ n)) * 1 <= ((vol A) / (2 |^ n)) * k1 by A16, A3, XREAL_1:64;

then ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * k1 by A46, XXREAL_0:2;

then A47: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A44, A26, XREAL_1:7;

now :: thesis: not k1 <> 1

then
( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 )
by A13, A19, INTEGRA1:def 4;assume A48:
k1 <> 1
; :: thesis: contradiction

then 1 < k1 by A16, XXREAL_0:1;

then k1 -' 1 >= 1 by NAT_1:14, NAT_D:36;

then ((vol A) / (2 |^ n)) * 1 <= ((vol A) / (2 |^ n)) * (k1 -' 1) by A3, XREAL_1:64;

then ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * (k1 -' 1) by A46, XXREAL_0:2;

then A49: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . (k1 -' 1) by A44, A26, A48, A32, XREAL_1:7;

end;then 1 < k1 by A16, XXREAL_0:1;

then k1 -' 1 >= 1 by NAT_1:14, NAT_D:36;

then ((vol A) / (2 |^ n)) * 1 <= ((vol A) / (2 |^ n)) * (k1 -' 1) by A3, XREAL_1:64;

then ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * (k1 -' 1) by A46, XXREAL_0:2;

then A49: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . (k1 -' 1) by A44, A26, A48, A32, XREAL_1:7;

per cases
( ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) or k1 = len (EqDiv (A,(2 |^ n))) )
by A48, A16, A15, XXREAL_0:1;

end;

suppose
( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) )
; :: thesis: contradiction

then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).[
by A13, A19;

then ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x < (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:3;

hence contradiction by A45, A49, XXREAL_0:2; :: thesis: verum

end;then ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x < (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:3;

hence contradiction by A45, A49, XXREAL_0:2; :: thesis: verum

suppose
k1 = len (EqDiv (A,(2 |^ n)))
; :: thesis: contradiction

then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).]
by A13, A19, A44;

then ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x <= (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:1;

hence contradiction by A45, A49, XXREAL_0:2; :: thesis: verum

end;then ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x <= (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:1;

hence contradiction by A45, A49, XXREAL_0:2; :: thesis: verum

then A50: divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound A),((EqDiv (A,(2 |^ n))) . k1).] by INTEGRA1:4;

( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A44, A14, A19, INTEGRA1:def 4;

then divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound A),((EqDiv (A,(2 |^ m))) . k2).] by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A47, A50, XXREAL_1:34; :: thesis: verum

suppose A51:
( len (EqDiv (A,(2 |^ n))) <> 1 & k2 = len (EqDiv (A,(2 |^ m))) )
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
Km . k2 = [.((EqDiv (A,(2 |^ m))) . (k2 -' 1)),((EqDiv (A,(2 |^ m))) . k2).]
by A14, A19, A42;

then A52: ( (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) <= x & x <= (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A26, A42, A51, A34, A17, XXREAL_1:1;

A61: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A26, A34, A18, A51, A42, A19, A14, INTEGRA1:def 4;

(2 |^ m) - (2 |^ (m -' n)) <= (2 |^ m) - 1 by A36, NAT_1:14, XREAL_1:10;

then ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A30, A53, A51, A25, A18, A3, XREAL_1:64;

then A62: lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) <= lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) by A38, A60, A61, XREAL_1:6;

( ((vol A) / (2 |^ n)) * k1 = (vol A) / ((2 |^ n) / (2 |^ n)) & ((vol A) / (2 |^ m)) * k2 = (vol A) / ((2 |^ m) / (2 |^ m)) ) by A53, A51, A25, XCMPLX_1:82;

then A63: ( ((vol A) / (2 |^ n)) * k1 = vol A & ((vol A) / (2 |^ m)) * k2 = vol A ) by A23, XCMPLX_1:51;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A60, A61, A62, A63, XXREAL_1:34; :: thesis: verum

end;then A52: ( (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) <= x & x <= (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A26, A42, A51, A34, A17, XXREAL_1:1;

A53: now :: thesis: not k1 <> len (EqDiv (A,(2 |^ n)))

then A60:
( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (lower_bound A) + (((vol A) / (2 |^ n)) * k1) )
by A26, A32, A51, A18, A19, A13, INTEGRA1:def 4;assume A54:
k1 <> len (EqDiv (A,(2 |^ n)))
; :: thesis: contradiction

end;per cases
( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) )
by A15, A16, A54, XXREAL_0:1;

end;

suppose A55:
k1 = 1
; :: thesis: contradiction

then
Kn . k1 = [.(inf A),((EqDiv (A,(2 |^ n))) . 1).[
by A51, A13, A19;

then ( inf A <= x & x < (EqDiv (A,(2 |^ n))) . 1 ) by A16, XXREAL_1:3;

then A56: x < (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) by A55, A26, A37, XCMPLX_1:82;

then (2 |^ (m -' n)) + 1 <= 2 |^ m by NAT_1:13;

then 2 |^ (m -' n) <= k2 -' 1 by A29, A51, A25, XREAL_1:19;

then ((vol A) / (2 |^ m)) * (2 |^ (m -' n)) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A52, A56, XXREAL_0:2; :: thesis: verum

end;then ( inf A <= x & x < (EqDiv (A,(2 |^ n))) . 1 ) by A16, XXREAL_1:3;

then A56: x < (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) by A55, A26, A37, XCMPLX_1:82;

now :: thesis: not 2 |^ (m -' n) = 2 |^ m

then
2 |^ (m -' n) < 2 |^ m
by A31, XXREAL_0:1;assume
2 |^ (m -' n) = 2 |^ m
; :: thesis: contradiction

then m -' n = m by PEPIN:30;

then 2 |^ n = 1 by A28, NEWTON:4;

hence contradiction by A51, A24, INTEGRA4:def 1; :: thesis: verum

end;then m -' n = m by PEPIN:30;

then 2 |^ n = 1 by A28, NEWTON:4;

hence contradiction by A51, A24, INTEGRA4:def 1; :: thesis: verum

then (2 |^ (m -' n)) + 1 <= 2 |^ m by NAT_1:13;

then 2 |^ (m -' n) <= k2 -' 1 by A29, A51, A25, XREAL_1:19;

then ((vol A) / (2 |^ m)) * (2 |^ (m -' n)) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A52, A56, XXREAL_0:2; :: thesis: verum

suppose A57:
( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) )
; :: thesis: contradiction

then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).[
by A13, A19;

then A58: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A26, A57, A32, A16, XXREAL_1:3;

k1 < len (EqDiv (A,(2 |^ n))) by A54, A15, A16, XXREAL_0:1;

then k1 + 1 <= 2 |^ n by A25, NAT_1:13;

then k1 <= (2 |^ n) - 1 by XREAL_1:19;

then A59: ((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ n)) * ((2 |^ n) - 1) by A3, XREAL_1:64;

(2 |^ m) - (2 |^ (m -' n)) <= k2 -' 1 by A29, A51, A25, A36, NAT_1:14, XREAL_1:10;

then ((vol A) / (2 |^ m)) * ((2 |^ (m -' n)) * ((2 |^ n) - 1)) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A30, A3, XREAL_1:64;

then ((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A38, A59, XXREAL_0:2;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A52, A58, XXREAL_0:2; :: thesis: verum

end;then A58: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A26, A57, A32, A16, XXREAL_1:3;

k1 < len (EqDiv (A,(2 |^ n))) by A54, A15, A16, XXREAL_0:1;

then k1 + 1 <= 2 |^ n by A25, NAT_1:13;

then k1 <= (2 |^ n) - 1 by XREAL_1:19;

then A59: ((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ n)) * ((2 |^ n) - 1) by A3, XREAL_1:64;

(2 |^ m) - (2 |^ (m -' n)) <= k2 -' 1 by A29, A51, A25, A36, NAT_1:14, XREAL_1:10;

then ((vol A) / (2 |^ m)) * ((2 |^ (m -' n)) * ((2 |^ n) - 1)) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A30, A3, XREAL_1:64;

then ((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A38, A59, XXREAL_0:2;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A52, A58, XXREAL_0:2; :: thesis: verum

A61: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (lower_bound A) + (((vol A) / (2 |^ m)) * k2) ) by A26, A34, A18, A51, A42, A19, A14, INTEGRA1:def 4;

(2 |^ m) - (2 |^ (m -' n)) <= (2 |^ m) - 1 by A36, NAT_1:14, XREAL_1:10;

then ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A30, A53, A51, A25, A18, A3, XREAL_1:64;

then A62: lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) <= lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) by A38, A60, A61, XREAL_1:6;

( ((vol A) / (2 |^ n)) * k1 = (vol A) / ((2 |^ n) / (2 |^ n)) & ((vol A) / (2 |^ m)) * k2 = (vol A) / ((2 |^ m) / (2 |^ m)) ) by A53, A51, A25, XCMPLX_1:82;

then A63: ( ((vol A) / (2 |^ n)) * k1 = vol A & ((vol A) / (2 |^ m)) * k2 = vol A ) by A23, XCMPLX_1:51;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A60, A61, A62, A63, XXREAL_1:34; :: thesis: verum

suppose A64:
( len (EqDiv (A,(2 |^ n))) <> 1 & k2 <> 1 & k2 <> len (EqDiv (A,(2 |^ m))) )
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then A65:
( 1 < k2 & k2 < len (EqDiv (A,(2 |^ m))) )
by A17, A15, XXREAL_0:1;

then Km . k2 = [.((EqDiv (A,(2 |^ m))) . (k2 -' 1)),((EqDiv (A,(2 |^ m))) . k2).[ by A14, A19;

then A66: ( (EqDiv (A,(2 |^ m))) . (k2 -' 1) <= x & x < (EqDiv (A,(2 |^ m))) . k2 ) by A17, XXREAL_1:3;

end;then Km . k2 = [.((EqDiv (A,(2 |^ m))) . (k2 -' 1)),((EqDiv (A,(2 |^ m))) . k2).[ by A14, A19;

then A66: ( (EqDiv (A,(2 |^ m))) . (k2 -' 1) <= x & x < (EqDiv (A,(2 |^ m))) . k2 ) by A17, XXREAL_1:3;

per cases
( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) or k1 = len (EqDiv (A,(2 |^ n))) )
by A16, A15, XXREAL_0:1;

end;

suppose A67:
k1 = 1
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
Kn . k1 = [.(inf A),((EqDiv (A,(2 |^ n))) . k1).[
by A64, A13, A19;

then A68: x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) by A26, A16, XXREAL_1:3;

then A70: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A26, XREAL_1:6;

A71: (inf A) + 0 <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A3, XREAL_1:6;

A72: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A67, INTEGRA1:def 4;

A73: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A34, A64, A70, A71, A72, A73, XXREAL_1:34; :: thesis: verum

end;then A68: x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) by A26, A16, XXREAL_1:3;

now :: thesis: not k1 * (2 |^ (m -' n)) < k2

then
((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1
by A39, A3, XREAL_1:64;assume
k1 * (2 |^ (m -' n)) < k2
; :: thesis: contradiction

then (k1 * (2 |^ (m -' n))) + 1 <= k2 by NAT_1:13;

then ((k1 * (2 |^ (m -' n))) + 1) -' 1 <= k2 -' 1 by NAT_D:42;

then A69: k1 * (2 |^ (m -' n)) <= k2 -' 1 by NAT_D:34;

((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A39, A69, A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A66, A68, A34, A64, XXREAL_0:2; :: thesis: verum

end;then (k1 * (2 |^ (m -' n))) + 1 <= k2 by NAT_1:13;

then ((k1 * (2 |^ (m -' n))) + 1) -' 1 <= k2 -' 1 by NAT_D:42;

then A69: k1 * (2 |^ (m -' n)) <= k2 -' 1 by NAT_D:34;

((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A39, A69, A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by XREAL_1:6;

hence contradiction by A66, A68, A34, A64, XXREAL_0:2; :: thesis: verum

then A70: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A26, XREAL_1:6;

A71: (inf A) + 0 <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A3, XREAL_1:6;

A72: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = lower_bound A & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A67, INTEGRA1:def 4;

A73: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A34, A64, A70, A71, A72, A73, XXREAL_1:34; :: thesis: verum

suppose A74:
( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) )
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).[
by A13, A19;

then A75: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A74, A26, A32, A16, XXREAL_1:3;

then A76: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A26, XREAL_1:6;

A77: k2 -' 1 >= 1 by A65, NAT_D:36, NAT_1:14;

then A78: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A32, A34, A74, A64, XREAL_1:6;

A79: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A18, A74, INTEGRA1:def 4;

A80: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A76, A78, A79, A80, XXREAL_1:34; :: thesis: verum

end;then A75: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A74, A26, A32, A16, XXREAL_1:3;

now :: thesis: not k1 * (2 |^ (m -' n)) < k2

then
((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1
by A39, A3, XREAL_1:64;assume
k1 * (2 |^ (m -' n)) < k2
; :: thesis: contradiction

then (k1 * (2 |^ (m -' n))) + 1 <= k2 by NAT_1:13;

then ((k1 * (2 |^ (m -' n))) + 1) -' 1 <= k2 -' 1 by NAT_D:42;

then k1 * (2 |^ (m -' n)) <= k2 -' 1 by NAT_D:34;

then ((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A38, XREAL_1:6;

hence contradiction by A66, A75, A34, A64, XXREAL_0:2; :: thesis: verum

end;then (k1 * (2 |^ (m -' n))) + 1 <= k2 by NAT_1:13;

then ((k1 * (2 |^ (m -' n))) + 1) -' 1 <= k2 -' 1 by NAT_D:42;

then k1 * (2 |^ (m -' n)) <= k2 -' 1 by NAT_D:34;

then ((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A38, XREAL_1:6;

hence contradiction by A66, A75, A34, A64, XXREAL_0:2; :: thesis: verum

then A76: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A26, XREAL_1:6;

A77: k2 -' 1 >= 1 by A65, NAT_D:36, NAT_1:14;

now :: thesis: not k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))

then
((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A39, A3, XREAL_1:64;assume
k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))
; :: thesis: contradiction

then (k2 -' 1) + 1 <= (k1 -' 1) * (2 |^ (m -' n)) by NAT_1:13;

then k2 <= (k1 -' 1) * (2 |^ (m -' n)) by A77, NAT_D:43;

then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * k2) <= (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A38, XREAL_1:6;

hence contradiction by A75, A66, A26, XXREAL_0:2; :: thesis: verum

end;then (k2 -' 1) + 1 <= (k1 -' 1) * (2 |^ (m -' n)) by NAT_1:13;

then k2 <= (k1 -' 1) * (2 |^ (m -' n)) by A77, NAT_D:43;

then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * k2) <= (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A38, XREAL_1:6;

hence contradiction by A75, A66, A26, XXREAL_0:2; :: thesis: verum

then A78: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A32, A34, A74, A64, XREAL_1:6;

A79: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A18, A74, INTEGRA1:def 4;

A80: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A76, A78, A79, A80, XXREAL_1:34; :: thesis: verum

suppose A81:
k1 = len (EqDiv (A,(2 |^ n)))
; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)

then
Kn . k1 = [.((EqDiv (A,(2 |^ n))) . (k1 -' 1)),((EqDiv (A,(2 |^ n))) . k1).]
by A64, A13, A19;

then A82: ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x <= (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:1;

A83: k2 -' 1 >= 1 by A65, NAT_D:36, NAT_1:14;

then A84: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A32, A34, A81, A64, XREAL_1:6;

A85: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A18, A81, A64, INTEGRA1:def 4;

A86: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

A87: ( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

A88: (EqDiv (A,(2 |^ m))) . (k2 -' 1) <= (EqDiv (A,(2 |^ m))) . k2 by A66, XXREAL_0:2;

divset ((EqDiv (A,(2 |^ m))),k2) c= A by A14, A19, INTEGRA1:8;

then divset ((EqDiv (A,(2 |^ m))),k2) c= [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) <= upper_bound A by A87, A88, A86, XXREAL_1:50;

then (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A86, A81, INTEGRA1:def 2;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A84, A85, A86, A87, XXREAL_1:34; :: thesis: verum

end;then A82: ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x <= (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:1;

A83: k2 -' 1 >= 1 by A65, NAT_D:36, NAT_1:14;

now :: thesis: not k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))

then
((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1)
by A39, A3, XREAL_1:64;assume
k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))
; :: thesis: contradiction

then (k2 -' 1) + 1 <= (k1 -' 1) * (2 |^ (m -' n)) by NAT_1:13;

then k2 <= (k1 -' 1) * (2 |^ (m -' n)) by A83, NAT_D:43;

then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * k2) <= (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A38, XREAL_1:6;

hence contradiction by A82, A66, A26, A64, A81, A32, XXREAL_0:2; :: thesis: verum

end;then (k2 -' 1) + 1 <= (k1 -' 1) * (2 |^ (m -' n)) by NAT_1:13;

then k2 <= (k1 -' 1) * (2 |^ (m -' n)) by A83, NAT_D:43;

then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) by A3, XREAL_1:64;

then (lower_bound A) + (((vol A) / (2 |^ m)) * k2) <= (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) by A38, XREAL_1:6;

hence contradiction by A82, A66, A26, A64, A81, A32, XXREAL_0:2; :: thesis: verum

then A84: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A32, A34, A81, A64, XREAL_1:6;

A85: ( lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . (k1 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ n))),k1)) = (EqDiv (A,(2 |^ n))) . k1 ) by A19, A13, A18, A81, A64, INTEGRA1:def 4;

A86: ( lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . (k2 -' 1) & upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) = (EqDiv (A,(2 |^ m))) . k2 ) by A19, A14, A18, A64, INTEGRA1:def 4;

A87: ( divset ((EqDiv (A,(2 |^ n))),k1) = [.(lower_bound (divset ((EqDiv (A,(2 |^ n))),k1))),(upper_bound (divset ((EqDiv (A,(2 |^ n))),k1))).] & divset ((EqDiv (A,(2 |^ m))),k2) = [.(lower_bound (divset ((EqDiv (A,(2 |^ m))),k2))),(upper_bound (divset ((EqDiv (A,(2 |^ m))),k2))).] ) by INTEGRA1:4;

A88: (EqDiv (A,(2 |^ m))) . (k2 -' 1) <= (EqDiv (A,(2 |^ m))) . k2 by A66, XXREAL_0:2;

divset ((EqDiv (A,(2 |^ m))),k2) c= A by A14, A19, INTEGRA1:8;

then divset ((EqDiv (A,(2 |^ m))),k2) c= [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then upper_bound (divset ((EqDiv (A,(2 |^ m))),k2)) <= upper_bound A by A87, A88, A86, XXREAL_1:50;

then (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A86, A81, INTEGRA1:def 2;

hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A84, A85, A86, A87, XXREAL_1:34; :: thesis: verum

hence (F . n) . x <= (F . m) . x by A16, A17, A21, A22, SEQ_4:47, RELAT_1:11; :: thesis: verum

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x )

proof

consider a, b being Real such that
let x be Element of REAL ; :: thesis: ( x in A implies ( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) )

assume A90: x in A ; :: thesis: ( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x )

for m, n being Nat st n <= m holds

(F # x) . n <= (F # x) . m

hence ( F # x is convergent & lim (F # x) = sup (F # x) ) by RINFSUP2:37; :: thesis: sup (F # x) <= f . x

for y being ExtReal st y in rng (F # x) holds

y <= f . x

then sup (rng (F # x)) <= f . x by XXREAL_2:def 3;

hence sup (F # x) <= f . x by RINFSUP2:def 1; :: thesis: verum

end;assume A90: x in A ; :: thesis: ( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x )

for m, n being Nat st n <= m holds

(F # x) . n <= (F # x) . m

proof

then
F # x is non-decreasing
by RINFSUP2:7;
let m, n be Nat; :: thesis: ( n <= m implies (F # x) . n <= (F # x) . m )

assume n <= m ; :: thesis: (F # x) . n <= (F # x) . m

then (F . n) . x <= (F . m) . x by A90, A9;

then (F # x) . n <= (F . m) . x by MESFUNC5:def 13;

hence (F # x) . n <= (F # x) . m by MESFUNC5:def 13; :: thesis: verum

end;assume n <= m ; :: thesis: (F # x) . n <= (F # x) . m

then (F . n) . x <= (F . m) . x by A90, A9;

then (F # x) . n <= (F . m) . x by MESFUNC5:def 13;

hence (F # x) . n <= (F # x) . m by MESFUNC5:def 13; :: thesis: verum

hence ( F # x is convergent & lim (F # x) = sup (F # x) ) by RINFSUP2:37; :: thesis: sup (F # x) <= f . x

for y being ExtReal st y in rng (F # x) holds

y <= f . x

proof

then
f . x is UpperBound of rng (F # x)
by XXREAL_2:def 1;
let y be ExtReal; :: thesis: ( y in rng (F # x) implies y <= f . x )

assume y in rng (F # x) ; :: thesis: y <= f . x

then consider n being Element of NAT such that

A91: ( n in dom (F # x) & y = (F # x) . n ) by PARTFUN1:3;

y = (F . n) . x by A91, MESFUNC5:def 13;

hence y <= f . x by A6, A90; :: thesis: verum

end;assume y in rng (F # x) ; :: thesis: y <= f . x

then consider n being Element of NAT such that

A91: ( n in dom (F # x) & y = (F # x) . n ) by PARTFUN1:3;

y = (F . n) . x by A91, MESFUNC5:def 13;

hence y <= f . x by A6, A90; :: thesis: verum

then sup (rng (F # x)) <= f . x by XXREAL_2:def 3;

hence sup (F # x) <= f . x by RINFSUP2:def 1; :: thesis: verum

A92: a <= b and

A93: A = [.a,b.] by MEASURE5:14;

reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;

A94: diameter A = b1 - a1 by A92, A93, MEASURE5:6;

B-Meas . A1 = diameter A by MEASUR12:71;

then A95: B-Meas . A1 < +infty by A94, XXREAL_0:4;

A96: for x being Element of REAL st x in A1 holds

F # x is convergent by A89;

A97: for n being Nat holds F . n is A1 -measurable by A8, MESFUNC2:34;

reconsider K = max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) as Real ;

A98: - |.(lower_bound (rng f)).| <= lower_bound (rng f) by ABSVALUE:4;

- K <= - |.(lower_bound (rng f)).| by XXREAL_0:25, XREAL_1:24;

then A99: - K <= lower_bound (rng f) by A98, XXREAL_0:2;

A100: upper_bound (rng f) <= |.(upper_bound (rng f)).| by ABSVALUE:4;

|.(upper_bound (rng f)).| <= K by XXREAL_0:25;

then A101: upper_bound (rng f) <= K by A100, XXREAL_0:2;

for n being Nat

for x being set st x in dom (F . 0) holds

|.((F . n) . x).| <= K

proof

then A105:
F is uniformly_bounded
by MESFUN10:def 1;
let n be Nat; :: thesis: for x being set st x in dom (F . 0) holds

|.((F . n) . x).| <= K

let x be set ; :: thesis: ( x in dom (F . 0) implies |.((F . n) . x).| <= K )

assume A102: x in dom (F . 0) ; :: thesis: |.((F . n) . x).| <= K

then reconsider x0 = x as Real ;

n is Element of NAT by ORDINAL1:def 12;

then A103: ( lower_bound (rng f) <= (F . n) . x0 & (F . n) . x0 <= f . x0 ) by A102, A6, A7;

A104: rng f is bounded_above by A1, SEQ_2:def 8, INTEGRA1:13;

reconsider K1 = K as ExtReal ;

f . x0 in rng f by A102, A2, A7, FUNCT_1:3;

then f . x0 <= upper_bound (rng f) by A104, SEQ_4:def 1;

then (F . n) . x0 <= upper_bound (rng f) by A103, XXREAL_0:2;

then ( - K <= (F . n) . x0 & (F . n) . x0 <= K ) by A99, A101, A103, XXREAL_0:2;

then ( - K1 <= (F . n) . x0 & (F . n) . x0 <= K1 ) by XXREAL_3:def 3;

hence |.((F . n) . x).| <= K by EXTREAL1:23; :: thesis: verum

end;|.((F . n) . x).| <= K

let x be set ; :: thesis: ( x in dom (F . 0) implies |.((F . n) . x).| <= K )

assume A102: x in dom (F . 0) ; :: thesis: |.((F . n) . x).| <= K

then reconsider x0 = x as Real ;

n is Element of NAT by ORDINAL1:def 12;

then A103: ( lower_bound (rng f) <= (F . n) . x0 & (F . n) . x0 <= f . x0 ) by A102, A6, A7;

A104: rng f is bounded_above by A1, SEQ_2:def 8, INTEGRA1:13;

reconsider K1 = K as ExtReal ;

f . x0 in rng f by A102, A2, A7, FUNCT_1:3;

then f . x0 <= upper_bound (rng f) by A104, SEQ_4:def 1;

then (F . n) . x0 <= upper_bound (rng f) by A103, XXREAL_0:2;

then ( - K <= (F . n) . x0 & (F . n) . x0 <= K ) by A99, A101, A103, XXREAL_0:2;

then ( - K1 <= (F . n) . x0 & (F . n) . x0 <= K1 ) by XXREAL_3:def 3;

hence |.((F . n) . x).| <= K by EXTREAL1:23; :: thesis: verum

then ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) by A96, A97, A95, A7, MESFUN10:19;

hence ex I being ExtREAL_sequence st

( A = dom (F . 0) & ( for n being Nat holds

( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = lower_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds

( lower_bound (rng f) <= (F . n) . x & (F . n) . x <= f . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of REAL st x in A holds

( F # x is convergent & lim (F # x) = sup (F # x) & sup (F # x) <= f . x ) ) & lim F is_integrable_on B-Meas & ( for n being Nat holds I . n = Integral (B-Meas,(F . n)) ) & I is convergent & lim I = Integral (B-Meas,(lim F)) ) by A7, A8, A9, A89, A105, A96, A97, A95, MESFUN10:19; :: thesis: verum