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 S1[ 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 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 = 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 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)) = 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
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;
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 = 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;
A34: 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 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;
A36: 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 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
per cases ( len (EqDiv (A,(2 |^ m))) = 1 or len (EqDiv (A,(2 |^ m))) <> 1 ) ;
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;
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 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
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;
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 A26, A42, A51, A34, A17, XXREAL_1:1;
A53: now :: thesis: not k1 <> len (EqDiv (A,(2 |^ n)))
assume A54: k1 <> len (EqDiv (A,(2 |^ n))) ; :: thesis: contradiction
per cases ( k1 = 1 or ( 1 < k1 & k1 < len (EqDiv (A,(2 |^ n))) ) ) by A15, A16, A54, XXREAL_0:1;
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;
now :: thesis: not 2 |^ (m -' n) = 2 |^ m
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 2 |^ (m -' n) < 2 |^ m by A31, XXREAL_0:1;
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;
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;
end;
end;
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;
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;
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;
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 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;
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 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 ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1 by A39, A3, XREAL_1:64;
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;
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;
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 A38, XREAL_1:6;
hence contradiction by A66, A75, A34, A64, XXREAL_0:2; :: thesis: verum
end;
then ((vol A) / (2 |^ m)) * k2 <= ((vol A) / (2 |^ n)) * k1 by A39, A3, XREAL_1:64;
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))
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 ((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A39, A3, XREAL_1:64;
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;
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;
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 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 ((vol A) / (2 |^ n)) * (k1 -' 1) <= ((vol A) / (2 |^ m)) * (k2 -' 1) by A39, A3, XREAL_1:64;
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;
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, A21, A22, SEQ_4:47, RELAT_1:11; :: thesis: verum
end;
A89: 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 )
proof
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
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 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;
then F # x is non-decreasing by RINFSUP2:7;
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
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;
then f . x is UpperBound of rng (F # x) by XXREAL_2:def 1;
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;
consider a, b being Real such that
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
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;
then A105: F is uniformly_bounded by MESFUN10:def 1;
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