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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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) = inf (F # x) & inf (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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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) = inf (F # x) & inf (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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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) = inf (F # x) & inf (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 S1[ Nat, PartFunc of REAL,ExtREAL] means ( A = dom $2 & $2 is_simple_func_in Borel_Sets & Integral (B-Meas,$2) = upper_sum (f,(EqDiv (A,(2 |^ $1)))) & ( for x being Real st x in A holds
( upper_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 = upper_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 S1[n,g]
proof
let n be Element of NAT ; :: thesis: ex g being Element of PFuncs (REAL,ExtREAL) st S1[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 = upper_bound (rng (f | (divset ((EqDiv (A,(2 |^ n))),k)))) ) ) & dom g = A & Integral (B-Meas,g) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_bound (rng f) >= g . x & g . x >= f . x ) ) ) by A1, A2, Th20;
g is Element of PFuncs (REAL,ExtREAL) by PARTFUN1:45;
hence ex g being Element of PFuncs (REAL,ExtREAL) st S1[n,g] by A5; :: thesis: verum
end;
consider F being Function of NAT,(PFuncs (REAL,ExtREAL)) such that
A6: for n being Element of NAT holds S1[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)
proof
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 ( S1[n,F . n] & S1[m,F . m] ) by A6;
hence dom (F . n) = dom (F . m) ; :: thesis: verum
end;
then reconsider F = F as with_the_same_dom Functional_Sequence of REAL,ExtREAL by MESFUNC8:def 2;
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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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) = inf (F # x) & inf (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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_bound (rng f) >= (F . n) . x & (F . n) . x >= f . x ) ) )
proof
let n be Nat; :: thesis: ( F . n is_simple_func_in Borel_Sets & Integral (B-Meas,(F . n)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_bound (rng f) >= (F . n) . x & (F . n) . x >= f . x ) ) ) by A6; :: thesis: verum
end;
A9: 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
proof
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 = upper_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 = upper_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 = upper_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 = upper_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;
then A21: dom (f | (divset ((EqDiv (A,(2 |^ n))),k1))) = divset ((EqDiv (A,(2 |^ n))),k1) by RELAT_1:62;
f = f | (dom f) ;
then f | (divset ((EqDiv (A,(2 |^ n))),k1)) is bounded by A1, A20, RFUNCT_1:74;
then rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is real-bounded by INTEGRA1:15;
then A22: ( not rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is empty & rng (f | (divset ((EqDiv (A,(2 |^ n))),k1))) is bounded_above ) by A21, RELAT_1:42;
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 A23: rng (f | (divset ((EqDiv (A,(2 |^ m))),k2))) <> {} by RELAT_1:42;
A24: ( 2 |^ n > 0 & 2 |^ m > 0 ) by NEWTON:83;
then A25: ( EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n & EqDiv (A,(2 |^ m)) divide_into_equal 2 |^ m ) by A3, Def1;
then A26: ( len (EqDiv (A,(2 |^ n))) = 2 |^ n & len (EqDiv (A,(2 |^ m))) = 2 |^ m ) by INTEGRA4:def 1;
then A27: ( (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 A25, A13, A14, A16, A17, FINSEQ_3:25, INTEGRA4:def 1;
A28: m - n >= 0 by A10, XREAL_1:48;
A29: m -' n = m - n by A10, XREAL_1:48, XREAL_0:def 2;
( 2 |^ n >= 1 & 2 |^ m >= 1 ) by A24, NAT_1:14;
then A30: ( (2 |^ n) -' 1 = (2 |^ n) - 1 & (2 |^ m) -' 1 = (2 |^ m) - 1 ) by XREAL_1:48, XREAL_0:def 2;
A31: (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 A28, NAT_D:72 ;
A32: 2 |^ (m -' n) <= 2 |^ m by NAT_D:35, PREPOWER:93;
A33: 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 A34: 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 A25, A26, A34, A13, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum
end;
A35: now :: thesis: ( 1 <> k2 implies (EqDiv (A,(2 |^ m))) . (k2 -' 1) = (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) )
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 A36: 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 A25, A26, A36, A14, FINSEQ_3:25, INTEGRA4:def 1; :: thesis: verum
end;
A37: 2 |^ (m -' n) > 0 by NEWTON:83;
( (2 |^ n) * (2 |^ (m -' n)) = 2 |^ m & (2 |^ n) * ((2 |^ (m -' n)) -' 1) < 2 |^ m ) by A10, Lm5;
then A38: 2 |^ n = (2 |^ m) / (2 |^ (m -' n)) by A37, XCMPLX_1:89;
then A39: (vol A) / (2 |^ n) = ((vol A) / (2 |^ m)) * (2 |^ (m -' n)) by XCMPLX_1:81;
then A40: ( ((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
per cases ( len (EqDiv (A,(2 |^ m))) = 1 or len (EqDiv (A,(2 |^ m))) <> 1 ) ;
suppose len (EqDiv (A,(2 |^ m))) = 1 ; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)
then A41: len (EqDiv (A,(2 |^ n))) = 1 by A26, A10, 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, Lm4;
hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A19, A14, INTEGRA1:8; :: thesis: verum
end;
suppose A42: len (EqDiv (A,(2 |^ m))) <> 1 ; :: thesis: divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1)
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))) ) ) ;
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;
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 A24, NAT_D:7;
then A46: ((vol A) / (2 |^ m)) * 1 <= ((vol A) / (2 |^ n)) * 1 by A3, A24, 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, A27, XREAL_1:7;
now :: thesis: not k1 <> 1
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, A27, A48, A33, 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;
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;
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;
end;
end;
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;
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;
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 A27, A42, A51, A35, A17, XXREAL_1:1;
A53: ((vol A) / (2 |^ n)) * ((2 |^ n) - 1) = (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) * ((2 |^ n) - 1) by A38, XCMPLX_1:81;
A54: now :: thesis: not k1 <> len (EqDiv (A,(2 |^ n)))
assume A55: k1 <> len (EqDiv (A,(2 |^ n))) ; :: thesis: contradiction
per cases ( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) ) by A15, A16, A55, XXREAL_0:1;
suppose A56: 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 A57: x < (lower_bound A) + (((vol A) / (2 |^ m)) * (2 |^ (m -' n))) by A56, A27, A38, XCMPLX_1:82;
now :: thesis: not 2 |^ (m -' n) = 2 |^ m
assume 2 |^ (m -' n) = 2 |^ m ; :: thesis: contradiction
then m - n = m by A29, PEPIN:30;
then 2 |^ n = 1 by NEWTON:4;
hence contradiction by A51, A25, INTEGRA4:def 1; :: thesis: verum
end;
then 2 |^ (m -' n) < 2 |^ m by A32, XXREAL_0:1;
then (2 |^ (m -' n)) + 1 <= 2 |^ m by NAT_1:13;
then 2 |^ (m -' n) <= k2 -' 1 by A30, A51, A26, 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, A57, XXREAL_0:2; :: thesis: verum
end;
suppose A58: ( 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 A59: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A27, A58, A33, A16, XXREAL_1:3;
k1 < len (EqDiv (A,(2 |^ n))) by A55, A15, A16, XXREAL_0:1;
then k1 + 1 <= 2 |^ n by A26, NAT_1:13;
then k1 <= (2 |^ n) - 1 by XREAL_1:19;
then A60: ((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 A30, A51, A26, A37, NAT_1:14, XREAL_1:10;
then ((vol A) / (2 |^ m)) * ((2 |^ (m -' n)) * ((2 |^ n) - 1)) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A31, A3, XREAL_1:64;
then ((vol A) / (2 |^ n)) * k1 <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A53, A60, 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, A59, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then A61: ( 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 A27, A33, A51, A18, A19, A13, INTEGRA1:def 4;
A62: ( 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 A27, A35, A18, A51, A42, A19, A14, INTEGRA1:def 4;
(2 |^ (m -' n)) * ((2 |^ n) - 1) <= (2 |^ m) - 1 by A31, A37, NAT_1:14, XREAL_1:10;
then ((vol A) / (2 |^ m)) * ((k1 -' 1) * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A54, A51, A26, A18, A3, XREAL_1:64;
then A63: lower_bound (divset ((EqDiv (A,(2 |^ n))),k1)) <= lower_bound (divset ((EqDiv (A,(2 |^ m))),k2)) by A53, A54, A18, A26, A61, A62, 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 A54, A51, A26, XCMPLX_1:82;
then A64: ( ((vol A) / (2 |^ n)) * k1 = vol A & ((vol A) / (2 |^ m)) * k2 = vol A ) by A24, 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 A61, A62, A63, A64, XXREAL_1:34; :: thesis: verum
end;
suppose A65: ( 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 A66: ( 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 A67: ( (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;
suppose A68: 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 A65, A13, A19;
then A69: x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) by A27, A16, XXREAL_1:3;
now :: thesis: not k1 * (2 |^ (m -' n)) < k2
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 A70: k1 * (2 |^ (m -' n)) <= k2 -' 1 by NAT_D:34;
((vol A) / (2 |^ m)) * (k1 * (2 |^ (m -' n))) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A70, A3, XREAL_1:64;
then (lower_bound A) + (((vol A) / (2 |^ n)) * k1) <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A39, XREAL_1:6;
hence contradiction by A67, A35, A65, A69, XXREAL_0:2; :: thesis: verum
end;
then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1 by A40, A3, XREAL_1:64;
then A71: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A27, XREAL_1:6;
A72: (inf A) + 0 <= (lower_bound A) + (((vol A) / (2 |^ m)) * (k2 -' 1)) by A3, XREAL_1:6;
A73: ( 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, A68, INTEGRA1:def 4;
A74: ( 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, A65, 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 A71, A72, A35, A65, A73, A74, XXREAL_1:34; :: thesis: verum
end;
suppose A75: ( 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 A76: ( (lower_bound A) + (((vol A) / (2 |^ n)) * (k1 -' 1)) <= x & x < (lower_bound A) + (((vol A) / (2 |^ n)) * k1) ) by A75, A27, A33, A16, XXREAL_1:3;
now :: thesis: not k1 * (2 |^ (m -' n)) < k2
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 A39, XREAL_1:6;
hence contradiction by A67, A35, A65, A76, XXREAL_0:2; :: thesis: verum
end;
then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1 by A40, A3, XREAL_1:64;
then A77: (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A27, XREAL_1:6;
A78: k2 -' 1 >= 1 by A66, NAT_D:36, NAT_1:14;
now :: thesis: not k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))
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 A78, 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 A39, XREAL_1:6;
hence contradiction by A76, A67, A27, XXREAL_0:2; :: thesis: verum
end;
then ((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A40, A3, XREAL_1:64;
then A79: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A33, A35, A75, A65, XREAL_1:6;
A80: ( 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, A75, INTEGRA1:def 4;
A81: ( 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, A65, 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 A77, A79, A80, A81, XXREAL_1:34; :: thesis: verum
end;
suppose A82: 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 A65, A13, A19;
then A83: ( (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= x & x <= (EqDiv (A,(2 |^ n))) . k1 ) by A16, XXREAL_1:1;
A84: k2 -' 1 >= 1 by A66, NAT_D:36, NAT_1:14;
now :: thesis: not k2 -' 1 < (k1 -' 1) * (2 |^ (m -' n))
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 A84, 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 A39, XREAL_1:6;
hence contradiction by A83, A67, A27, A65, A82, A33, XXREAL_0:2; :: thesis: verum
end;
then ((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A40, A3, XREAL_1:64;
then A85: (EqDiv (A,(2 |^ n))) . (k1 -' 1) <= (EqDiv (A,(2 |^ m))) . (k2 -' 1) by A33, A35, A82, A65, XREAL_1:6;
A86: ( 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, A82, A65, INTEGRA1:def 4;
A87: ( 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, A65, INTEGRA1:def 4;
A88: ( 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;
A89: (EqDiv (A,(2 |^ m))) . (k2 -' 1) <= (EqDiv (A,(2 |^ m))) . k2 by A67, 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 A88, A89, A87, XXREAL_1:50;
then (EqDiv (A,(2 |^ m))) . k2 <= (EqDiv (A,(2 |^ n))) . k1 by A87, A82, INTEGRA1:def 2;
hence divset ((EqDiv (A,(2 |^ m))),k2) c= divset ((EqDiv (A,(2 |^ n))),k1) by A85, A86, A87, A88, XXREAL_1:34; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
then f | (divset ((EqDiv (A,(2 |^ m))),k2)) c= f | (divset ((EqDiv (A,(2 |^ n))),k1)) by RELAT_1:75;
hence (F . n) . x >= (F . m) . x by A16, A17, A22, A23, SEQ_4:48, RELAT_1:11; :: thesis: verum
end;
A90: for x being Element of REAL st x in A holds
( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x )
proof
let x be Element of REAL ; :: thesis: ( x in A implies ( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x ) )
assume A91: x in A ; :: thesis: ( F # x is convergent & lim (F # x) = inf (F # x) & inf (F # x) >= f . x )
for m, n being Nat st n <= m holds
(F # x) . n >= (F # x) . m
proof
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 A91, 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;
then F # x is non-increasing by RINFSUP2:7;
hence ( F # x is convergent & lim (F # x) = inf (F # x) ) by RINFSUP2:36; :: thesis: inf (F # x) >= f . x
for y being ExtReal st y in rng (F # x) holds
y >= f . x
proof
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
A92: ( n in dom (F # x) & y = (F # x) . n ) by PARTFUN1:3;
y = (F . n) . x by A92, MESFUNC5:def 13;
hence y >= f . x by A6, A91; :: thesis: verum
end;
then f . x is LowerBound of rng (F # x) by XXREAL_2:def 2;
then inf (rng (F # x)) >= f . x by XXREAL_2:def 4;
hence inf (F # x) >= f . x by RINFSUP2:def 2; :: thesis: verum
end;
consider a, b being Real such that
A93: a <= b and
A94: A = [.a,b.] by MEASURE5:14;
reconsider a1 = a, b1 = b as R_eal by XXREAL_0:def 1;
A95: diameter A = b1 - a1 by A93, A94, MEASURE5:6;
B-Meas . A1 = diameter A by MEASUR12:71;
then A96: B-Meas . A1 < +infty by A95, XXREAL_0:4;
A97: for x being Element of REAL st x in A1 holds
F # x is convergent by A90;
A98: for n being Nat holds F . n is A1 -measurable by A8, MESFUNC2:34;
set K = max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|);
A99: - |.(lower_bound (rng f)).| <= lower_bound (rng f) by ABSVALUE:4;
- (max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)) <= - |.(lower_bound (rng f)).| by XXREAL_0:25, XREAL_1:24;
then A100: - (max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)) <= lower_bound (rng f) by A99, XXREAL_0:2;
A101: upper_bound (rng f) <= |.(upper_bound (rng f)).| by ABSVALUE:4;
|.(upper_bound (rng f)).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) by XXREAL_0:25;
then A102: upper_bound (rng f) <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) by A101, XXREAL_0:2;
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)
proof
let n be Nat; :: thesis: for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)
let x be set ; :: thesis: ( x in dom (F . 0) implies |.((F . n) . x).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) )
assume A103: x in dom (F . 0) ; :: thesis: |.((F . n) . x).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)
then reconsider x0 = x as Real ;
n is Element of NAT by ORDINAL1:def 12;
then A104: ( upper_bound (rng f) >= (F . n) . x0 & (F . n) . x0 >= f . x0 ) by A103, A7, A6;
A105: rng f is bounded_below by A1, SEQ_2:def 8, INTEGRA1:11;
reconsider K1 = max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) as ExtReal ;
f . x0 in rng f by A103, A7, A2, FUNCT_1:3;
then f . x0 >= lower_bound (rng f) by A105, SEQ_4:def 2;
then (F . n) . x0 >= lower_bound (rng f) by A104, XXREAL_0:2;
then ( - (max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|)) <= (F . n) . x0 & (F . n) . x0 <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) ) by A100, A102, A104, XXREAL_0:2;
then ( - K1 <= (F . n) . x0 & (F . n) . x0 <= K1 ) by XXREAL_3:def 3;
hence |.((F . n) . x).| <= max (|.(lower_bound (rng f)).|,|.(upper_bound (rng f)).|) by EXTREAL1:23; :: thesis: verum
end;
then A106: F is uniformly_bounded by MESFUN10:def 1;
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 A97, A98, A96, A7, A106, 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)) = upper_sum (f,(EqDiv (A,(2 |^ n)))) & ( for x being Real st x in A holds
( upper_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) = inf (F # x) & inf (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, A90, A106, A97, A98, A96, MESFUN10:19; :: thesis: verum