let A be non empty closed_interval Subset of REAL; :: thesis: for A1 being Element of L-Field

for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

let A1 be Element of L-Field ; :: thesis: for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

let f be PartFunc of REAL,REAL; :: thesis: ( A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A implies ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) ) )

assume that

A1: A = A1 and

A2: A c= dom f and

A3: f || A is bounded and

A4: f is_integrable_on A ; :: thesis: ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

f || A is total by A2, INTEGRA5:6;

then reconsider g = f || A as Function of A,REAL ;

consider a, b being Real such that

A5: a <= b and

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

f || A is integrable by A4, INTEGRA5:def 1;

then A7: ( f || A is upper_integrable & f || A is lower_integrable & upper_integral (f || A) = lower_integral (f || A) ) by INTEGRA1:def 16;

for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

let A1 be Element of L-Field ; :: thesis: for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds

( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

let f be PartFunc of REAL,REAL; :: thesis: ( A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A implies ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) ) )

assume that

A1: A = A1 and

A2: A c= dom f and

A3: f || A is bounded and

A4: f is_integrable_on A ; :: thesis: ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

f || A is total by A2, INTEGRA5:6;

then reconsider g = f || A as Function of A,REAL ;

consider a, b being Real such that

A5: a <= b and

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

f || A is integrable by A4, INTEGRA5:def 1;

then A7: ( f || A is upper_integrable & f || A is lower_integrable & upper_integral (f || A) = lower_integral (f || A) ) by INTEGRA1:def 16;

per cases
( a = b or a <> b )
;

end;

suppose A8:
a = b
; :: thesis: ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

then A9:
A = {a}
by A6, XXREAL_1:17;

then consider AA being Element of Borel_Sets such that

A10: AA = {a} and

A11: f is AA -measurable and

A12: f | AA is_integrable_on B-Meas and

A13: Integral (B-Meas,(f | AA)) = 0 by A2, Th46, ZFMISC_1:31;

R_EAL f is AA -measurable by A11, MESFUNC6:def 1;

hence f is A1 -measurable by A1, A9, A10, Th30, MEASUR12:def 11, MESFUNC6:def 1; :: thesis: ( f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

thus f | A1 is_integrable_on L-Meas by A1, A9, A10, A12, Th48; :: thesis: integral (f || A) = Integral (L-Meas,(f | A))

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then ( a = lower_bound A & b = upper_bound A ) by A6, INTEGRA1:5;

then vol A = b - a by INTEGRA1:def 5;

then integral (f || A) = 0 by A8, INTEGRA4:6;

hence integral (f || A) = Integral (L-Meas,(f | A)) by A9, A10, A12, A13, Th48; :: thesis: verum

end;then consider AA being Element of Borel_Sets such that

A10: AA = {a} and

A11: f is AA -measurable and

A12: f | AA is_integrable_on B-Meas and

A13: Integral (B-Meas,(f | AA)) = 0 by A2, Th46, ZFMISC_1:31;

R_EAL f is AA -measurable by A11, MESFUNC6:def 1;

hence f is A1 -measurable by A1, A9, A10, Th30, MEASUR12:def 11, MESFUNC6:def 1; :: thesis: ( f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

thus f | A1 is_integrable_on L-Meas by A1, A9, A10, A12, Th48; :: thesis: integral (f || A) = Integral (L-Meas,(f | A))

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then ( a = lower_bound A & b = upper_bound A ) by A6, INTEGRA1:5;

then vol A = b - a by INTEGRA1:def 5;

then integral (f || A) = 0 by A8, INTEGRA4:6;

hence integral (f || A) = Integral (L-Meas,(f | A)) by A9, A10, A12, A13, Th48; :: thesis: verum

suppose
a <> b
; :: thesis: ( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

then A14:
a < b
by A5, XXREAL_0:1;

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then ( a = lower_bound A & b = upper_bound A ) by A6, INTEGRA1:5;

then A15: vol A = b - a by INTEGRA1:def 5;

then A16: vol A > 0 by A14, XREAL_1:50;

f || A is total by A2, INTEGRA5:6;

then A17: dom (f || A) = A by PARTFUN1:def 2;

consider F1 being with_the_same_dom Functional_Sequence of REAL,ExtREAL, I1 being ExtREAL_sequence such that

A18: ( A = dom (F1 . 0) & ( for n being Nat holds

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

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

for x being Element of REAL st x in A holds

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

( F1 # x is convergent & lim (F1 # x) = sup (F1 # x) & sup (F1 # x) <= (f || A) . x ) ) & lim F1 is_integrable_on B-Meas & ( for n being Nat holds I1 . n = Integral (B-Meas,(F1 . n)) ) & I1 is convergent & lim I1 = Integral (B-Meas,(lim F1)) ) by A3, A17, A15, Th21, A14, XREAL_1:50;

consider F2 being with_the_same_dom Functional_Sequence of REAL,ExtREAL, I2 being ExtREAL_sequence such that

A19: ( A = dom (F2 . 0) & ( for n being Nat holds

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

( upper_bound (rng (f || A)) >= (F2 . n) . x & (F2 . n) . x >= (f || A) . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

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

( F2 # x is convergent & lim (F2 # x) = inf (F2 # x) & inf (F2 # x) >= (f || A) . x ) ) & lim F2 is_integrable_on B-Meas & ( for n being Nat holds I2 . n = Integral (B-Meas,(F2 . n)) ) & I2 is convergent & lim I2 = Integral (B-Meas,(lim F2)) ) by A3, A17, A15, Th22, A14, XREAL_1:50;

A20: for n being Nat holds

( (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I2 . n & (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n )_{1}[ Element of NAT , object ] means $2 = EqDiv (A,(2 |^ $1));

A21: for n being Element of NAT ex D being Element of divs A st S_{1}[n,D]

A22: for n being Element of NAT holds S_{1}[n,T . n]
from FUNCT_2:sch 3(A21);

A23: for n being Nat holds T . n = EqDiv (A,(2 |^ n))

A25: ( delta T is 0 -convergent & delta T is non-zero ) by A16, A23, Th17;

then A26: ( upper_sum (g,T) is convergent & lim (upper_sum (g,T)) = upper_integral g ) by A16, A24, INTEGRA3:26;

A27: ( lower_sum (g,T) is convergent & lim (lower_sum (g,T)) = lower_integral g ) by A16, A24, A25, INTEGRA3:25;

for n being Element of NAT holds I1 . n = (lower_sum ((f || A),T)) . n

then A28: lim I1 = lower_integral (f || A) by A27, RINFSUP2:14;

for n being Element of NAT holds I2 . n = (upper_sum ((f || A),T)) . n

then A29: lim I2 = upper_integral (f || A) by A26, RINFSUP2:14;

A30: for x being Element of REAL st x in A holds

(lim F1) . x <= (f || A) . x

-infty < (lim F1) . x

+infty > (lim F1) . x

then reconsider Lf1 = lim F1 as PartFunc of REAL,REAL by Th3;

A42: for x being set st x in dom (lim F2) holds

+infty > (lim F2) . x

-infty < (lim F2) . x

then reconsider Lf2 = lim F2 as PartFunc of REAL,REAL by Th3;

A50: R_EAL Lf2 = lim F2 by MESFUNC5:def 7;

( (lim F2) - (lim F1) is V171() & (lim F2) - (lim F1) is V172() ) by A41, A42, A46, MESFUNC5:10, MESFUNC5:11, MESFUNC9:5, MESFUNC9:6;

then reconsider Lf3 = (lim F2) - (lim F1) as PartFunc of REAL,REAL by Th3;

A51: R_EAL Lf3 = (lim F2) - (lim F1) by MESFUNC5:def 7;

A52: dom (Lf2 - Lf1) = (dom (lim F2)) /\ (dom (lim F1)) by VALUED_1:12

.= dom Lf3 by A41, A46, MESFUNC5:10, MESFUNC5:17 ;

for x being Element of REAL st x in dom (Lf2 - Lf1) holds

(Lf2 - Lf1) . x = Lf3 . x

A56: for x being Element of REAL st x in A holds

(lim F2) . x >= (f || A) . x

A60: ( dom (lim F1) = A & dom (lim F2) = A ) by A18, A19, MESFUNC8:def 9;

A61: for x being Element of REAL st x in dom |.((lim F2) - (lim F1)).| holds

|.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x

reconsider A2 = A as Subset of REAL ;

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

Integral (B-Meas,|.((lim F2) - (lim F1)).|) = Integral (B-Meas,((lim F2) - (lim F1))) by A61, A59, PARTFUN1:5

.= (Integral (B-Meas,((lim F2) | ((dom (lim F2)) /\ (dom (lim F1)))))) - (Integral (B-Meas,((lim F1) | ((dom (lim F2)) /\ (dom (lim F1)))))) by A18, A19, MESFUN13:17

.= (lim I2) + (- (lim I2)) by A29, A7, A18, A19, A28, A60, XXREAL_3:def 4

.= 0 by XXREAL_3:7 ;

then A66: Integral (B-Meas,Lf3) = 0 by A65, MESFUNC6:def 3;

A67: Lf2 is_integrable_on B-Meas by A19, A50, MESFUNC6:def 4;

consider ELf2 being Element of Borel_Sets such that

A68: ( ELf2 = dom (R_EAL Lf2) & R_EAL Lf2 is ELf2 -measurable ) by A19, A50, MESFUNC5:def 17;

R_EAL f = f by MESFUNC5:def 7;

then A69: (R_EAL f) | A1 = R_EAL (f | A1) by MESFUNC5:def 7;

A70: Lf2 | A1 is A1 -measurable by A1, A60, A50, A68, Th30, MEASUR12:def 11, MESFUNC6:def 1;

reconsider z = 0 as Element of REAL by XREAL_0:def 1;

A71: dom Lf3 = (dom (lim F2)) /\ (dom (lim F1)) by A41, A46, MESFUNC5:10, MESFUNC5:17;

A72: for x being Element of REAL st x in A holds

Lf2 . x >= f . x

f . x >= Lf1 . x

Lf3 . x >= 0

A79: R_EAL Lf3 = Lf3 by MESFUNC5:def 7;

R_EAL Lf3 is_integrable_on B-Meas by A51, A18, A19, MESFUN10:12;

then ex ELf3 being Element of Borel_Sets st

( ELf3 = dom (R_EAL Lf3) & R_EAL Lf3 is ELf3 -measurable ) by MESFUNC5:def 17;

then Lf3 is A3 -measurable by A79, A71, A60, A1, MESFUNC6:def 1;

then A80: Lf3 a.e.= (REAL --> 0) | A1, L-Meas by A1, A66, A71, A60, A78, Th25, Th29;

consider E0 being Element of L-Field such that

A82: ( L-Meas . E0 = 0 & Lf3 | (E0 `) = ((REAL --> 0) | A1) | (E0 `) ) by A80, LPSPACE1:def 10;

dom (Lf2 - f) = (dom Lf2) /\ (dom f) by VALUED_1:12;

then A81: dom (Lf2 - f) = A1 by A1, A60, A2, XBOOLE_1:28;

then A83: dom ((Lf2 - f) | (E0 `)) = A1 /\ (E0 `) by RELAT_1:61;

dom ((REAL --> 0) | A1) = (dom (REAL --> 0)) /\ A1 by RELAT_1:61;

then dom ((REAL --> 0) | A1) = A1 by XBOOLE_1:28;

then A84: dom (((REAL --> 0) | A1) | (E0 `)) = A1 /\ (E0 `) by RELAT_1:61;

for x being Element of REAL st x in dom ((Lf2 - f) | (E0 `)) holds

((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x

then A90: Lf2 | A1 a.e.= f | A1, L-Meas by A81, A82, Th40, LPSPACE1:def 10;

then (R_EAL f) | A1 is A1 -measurable by A69, A1, A60, A70, Th26, MESFUNC6:def 1;

hence f is A1 -measurable by MESFUN13:19, MESFUNC6:def 1; :: thesis: ( f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

dom (f | A1) = (dom f) /\ A1 by RELAT_1:61;

then A91: dom (f | A1) = A1 by A1, A2, XBOOLE_1:28;

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

L-Meas . A1 = diameter A by A1, MEASUR12:76;

then L-Meas . A1 = b1 - a1 by A5, A6, MEASURE5:6;

then L-Meas . A1 < +infty by XXREAL_0:9, XREAL_0:def 1;

hence f | A1 is_integrable_on L-Meas by A1, A3, A90, A60, A70, A91, Th26, Th41; :: thesis: integral (f || A) = Integral (L-Meas,(f | A))

integral (f || A) = lim I2 by A29, INTEGRA1:def 17;

then integral (f || A) = Integral (L-Meas,(lim F2)) by A19, Th38, MEASUR12:def 11, MEASUR12:def 12;

then A92: integral (f || A) = Integral (L-Meas,Lf2) by A50, MESFUNC6:def 3;

Lf2 is_integrable_on L-Meas by A67, Th48;

hence integral (f || A) = Integral (L-Meas,(f | A)) by A1, A60, A90, A91, A92, Th44; :: thesis: verum

end;A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;

then ( a = lower_bound A & b = upper_bound A ) by A6, INTEGRA1:5;

then A15: vol A = b - a by INTEGRA1:def 5;

then A16: vol A > 0 by A14, XREAL_1:50;

f || A is total by A2, INTEGRA5:6;

then A17: dom (f || A) = A by PARTFUN1:def 2;

consider F1 being with_the_same_dom Functional_Sequence of REAL,ExtREAL, I1 being ExtREAL_sequence such that

A18: ( A = dom (F1 . 0) & ( for n being Nat holds

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

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

for x being Element of REAL st x in A holds

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

( F1 # x is convergent & lim (F1 # x) = sup (F1 # x) & sup (F1 # x) <= (f || A) . x ) ) & lim F1 is_integrable_on B-Meas & ( for n being Nat holds I1 . n = Integral (B-Meas,(F1 . n)) ) & I1 is convergent & lim I1 = Integral (B-Meas,(lim F1)) ) by A3, A17, A15, Th21, A14, XREAL_1:50;

consider F2 being with_the_same_dom Functional_Sequence of REAL,ExtREAL, I2 being ExtREAL_sequence such that

A19: ( A = dom (F2 . 0) & ( for n being Nat holds

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

( upper_bound (rng (f || A)) >= (F2 . n) . x & (F2 . n) . x >= (f || A) . x ) ) ) ) & ( for n, m being Nat st n <= m holds

for x being Element of REAL st x in A holds

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

( F2 # x is convergent & lim (F2 # x) = inf (F2 # x) & inf (F2 # x) >= (f || A) . x ) ) & lim F2 is_integrable_on B-Meas & ( for n being Nat holds I2 . n = Integral (B-Meas,(F2 . n)) ) & I2 is convergent & lim I2 = Integral (B-Meas,(lim F2)) ) by A3, A17, A15, Th22, A14, XREAL_1:50;

A20: for n being Nat holds

( (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I2 . n & (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n )

proof

defpred S
let n be Nat; :: thesis: ( (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I2 . n & (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n )

(upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = upper_sum ((f || A),(EqDiv (A,(2 |^ n)))) by INTEGRA1:def 10

.= Integral (B-Meas,(F2 . n)) by A19 ;

hence (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I2 . n by A19; :: thesis: (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n

(lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = lower_sum ((f || A),(EqDiv (A,(2 |^ n)))) by INTEGRA1:def 11

.= Integral (B-Meas,(F1 . n)) by A18 ;

hence (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n by A18; :: thesis: verum

end;(upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = upper_sum ((f || A),(EqDiv (A,(2 |^ n)))) by INTEGRA1:def 10

.= Integral (B-Meas,(F2 . n)) by A19 ;

hence (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I2 . n by A19; :: thesis: (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n

(lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = lower_sum ((f || A),(EqDiv (A,(2 |^ n)))) by INTEGRA1:def 11

.= Integral (B-Meas,(F1 . n)) by A18 ;

hence (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) = I1 . n by A18; :: thesis: verum

A21: for n being Element of NAT ex D being Element of divs A st S

proof

consider T being Function of NAT,(divs A) such that
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S_{1}[n,D]

reconsider D = EqDiv (A,(2 |^ n)) as Element of divs A by INTEGRA1:def 3;

take D ; :: thesis: S_{1}[n,D]

thus S_{1}[n,D]
; :: thesis: verum

end;reconsider D = EqDiv (A,(2 |^ n)) as Element of divs A by INTEGRA1:def 3;

take D ; :: thesis: S

thus S

A22: for n being Element of NAT holds S

A23: for n being Nat holds T . n = EqDiv (A,(2 |^ n))

proof

A24:
(f || A) | A is bounded
by A3;
let n be Nat; :: thesis: T . n = EqDiv (A,(2 |^ n))

n is Element of NAT by ORDINAL1:def 12;

hence T . n = EqDiv (A,(2 |^ n)) by A22; :: thesis: verum

end;n is Element of NAT by ORDINAL1:def 12;

hence T . n = EqDiv (A,(2 |^ n)) by A22; :: thesis: verum

A25: ( delta T is 0 -convergent & delta T is non-zero ) by A16, A23, Th17;

then A26: ( upper_sum (g,T) is convergent & lim (upper_sum (g,T)) = upper_integral g ) by A16, A24, INTEGRA3:26;

A27: ( lower_sum (g,T) is convergent & lim (lower_sum (g,T)) = lower_integral g ) by A16, A24, A25, INTEGRA3:25;

for n being Element of NAT holds I1 . n = (lower_sum ((f || A),T)) . n

proof

then
I1 = lower_sum ((f || A),T)
by FUNCT_2:def 7;
let n be Element of NAT ; :: thesis: I1 . n = (lower_sum ((f || A),T)) . n

I1 . n = (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) by A20

.= (lower_sum_set (f || A)) . (T . n) by A23

.= lower_sum ((f || A),(T . n)) by INTEGRA1:def 11 ;

hence I1 . n = (lower_sum ((f || A),T)) . n by INTEGRA2:def 3; :: thesis: verum

end;I1 . n = (lower_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) by A20

.= (lower_sum_set (f || A)) . (T . n) by A23

.= lower_sum ((f || A),(T . n)) by INTEGRA1:def 11 ;

hence I1 . n = (lower_sum ((f || A),T)) . n by INTEGRA2:def 3; :: thesis: verum

then A28: lim I1 = lower_integral (f || A) by A27, RINFSUP2:14;

for n being Element of NAT holds I2 . n = (upper_sum ((f || A),T)) . n

proof

then
I2 = upper_sum ((f || A),T)
by FUNCT_2:def 7;
let n be Element of NAT ; :: thesis: I2 . n = (upper_sum ((f || A),T)) . n

I2 . n = (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) by A20

.= (upper_sum_set (f || A)) . (T . n) by A23

.= upper_sum ((f || A),(T . n)) by INTEGRA1:def 10 ;

hence I2 . n = (upper_sum ((f || A),T)) . n by INTEGRA2:def 2; :: thesis: verum

end;I2 . n = (upper_sum_set (f || A)) . (EqDiv (A,(2 |^ n))) by A20

.= (upper_sum_set (f || A)) . (T . n) by A23

.= upper_sum ((f || A),(T . n)) by INTEGRA1:def 10 ;

hence I2 . n = (upper_sum ((f || A),T)) . n by INTEGRA2:def 2; :: thesis: verum

then A29: lim I2 = upper_integral (f || A) by A26, RINFSUP2:14;

A30: for x being Element of REAL st x in A holds

(lim F1) . x <= (f || A) . x

proof

A33:
for x being set st x in dom (lim F1) holds
let x be Element of REAL ; :: thesis: ( x in A implies (lim F1) . x <= (f || A) . x )

assume A31: x in A ; :: thesis: (lim F1) . x <= (f || A) . x

then A32: x in dom (lim F1) by A18, MESFUNC8:def 9;

lim (F1 # x) = sup (F1 # x) by A31, A18;

then lim (F1 # x) <= (f || A) . x by A31, A18;

hence (lim F1) . x <= (f || A) . x by A32, MESFUNC8:def 9; :: thesis: verum

end;assume A31: x in A ; :: thesis: (lim F1) . x <= (f || A) . x

then A32: x in dom (lim F1) by A18, MESFUNC8:def 9;

lim (F1 # x) = sup (F1 # x) by A31, A18;

then lim (F1 # x) <= (f || A) . x by A31, A18;

hence (lim F1) . x <= (f || A) . x by A32, MESFUNC8:def 9; :: thesis: verum

-infty < (lim F1) . x

proof

A37:
for x being set st x in dom (lim F1) holds
let x be set ; :: thesis: ( x in dom (lim F1) implies -infty < (lim F1) . x )

assume A34: x in dom (lim F1) ; :: thesis: -infty < (lim F1) . x

then reconsider x1 = x as Element of REAL ;

A35: x in A by A34, A18, MESFUNC8:def 9;

then lim (F1 # x1) = sup (F1 # x1) by A18;

then (lim F1) . x = sup (F1 # x1) by A34, MESFUNC8:def 9;

then (F1 # x1) . 0 <= (lim F1) . x by RINFSUP2:23;

then A36: (F1 . 0) . x1 <= (lim F1) . x by MESFUNC5:def 13;

lower_bound (rng (f || A)) <= (F1 . 0) . x1 by A35, A18;

then lower_bound (rng (f || A)) <= (lim F1) . x by A36, XXREAL_0:2;

hence -infty < (lim F1) . x by XXREAL_0:2, XXREAL_0:6; :: thesis: verum

end;assume A34: x in dom (lim F1) ; :: thesis: -infty < (lim F1) . x

then reconsider x1 = x as Element of REAL ;

A35: x in A by A34, A18, MESFUNC8:def 9;

then lim (F1 # x1) = sup (F1 # x1) by A18;

then (lim F1) . x = sup (F1 # x1) by A34, MESFUNC8:def 9;

then (F1 # x1) . 0 <= (lim F1) . x by RINFSUP2:23;

then A36: (F1 . 0) . x1 <= (lim F1) . x by MESFUNC5:def 13;

lower_bound (rng (f || A)) <= (F1 . 0) . x1 by A35, A18;

then lower_bound (rng (f || A)) <= (lim F1) . x by A36, XXREAL_0:2;

hence -infty < (lim F1) . x by XXREAL_0:2, XXREAL_0:6; :: thesis: verum

+infty > (lim F1) . x

proof

A41:
( lim F1 is V171() & lim F1 is V172() )
by A33, A37, MESFUNC5:10, MESFUNC5:11;
let x be set ; :: thesis: ( x in dom (lim F1) implies +infty > (lim F1) . x )

assume A38: x in dom (lim F1) ; :: thesis: +infty > (lim F1) . x

then reconsider x1 = x as Element of REAL ;

A39: x in A by A38, A18, MESFUNC8:def 9;

then lim (F1 # x1) = sup (F1 # x1) by A18;

then (lim F1) . x = sup (F1 # x1) by A38, MESFUNC8:def 9;

then (lim F1) . x <= (f || A) . x1 by A39, A18;

then A40: (lim F1) . x <= f . x1 by A39, FUNCT_1:49;

f . x1 in REAL by A2, A39, PARTFUN1:4;

hence +infty > (lim F1) . x by A40, XXREAL_0:2, XXREAL_0:9; :: thesis: verum

end;assume A38: x in dom (lim F1) ; :: thesis: +infty > (lim F1) . x

then reconsider x1 = x as Element of REAL ;

A39: x in A by A38, A18, MESFUNC8:def 9;

then lim (F1 # x1) = sup (F1 # x1) by A18;

then (lim F1) . x = sup (F1 # x1) by A38, MESFUNC8:def 9;

then (lim F1) . x <= (f || A) . x1 by A39, A18;

then A40: (lim F1) . x <= f . x1 by A39, FUNCT_1:49;

f . x1 in REAL by A2, A39, PARTFUN1:4;

hence +infty > (lim F1) . x by A40, XXREAL_0:2, XXREAL_0:9; :: thesis: verum

then reconsider Lf1 = lim F1 as PartFunc of REAL,REAL by Th3;

A42: for x being set st x in dom (lim F2) holds

+infty > (lim F2) . x

proof

A46:
for x being set st x in dom (lim F2) holds
let x be set ; :: thesis: ( x in dom (lim F2) implies +infty > (lim F2) . x )

assume A43: x in dom (lim F2) ; :: thesis: +infty > (lim F2) . x

then reconsider x1 = x as Element of REAL ;

A44: x in A by A43, A19, MESFUNC8:def 9;

then lim (F2 # x1) = inf (F2 # x1) by A19;

then (lim F2) . x = inf (F2 # x1) by A43, MESFUNC8:def 9;

then (F2 # x1) . 0 >= (lim F2) . x by RINFSUP2:23;

then A45: (F2 . 0) . x1 >= (lim F2) . x by MESFUNC5:def 13;

upper_bound (rng (f || A)) >= (F2 . 0) . x1 by A44, A19;

then upper_bound (rng (f || A)) >= (lim F2) . x by A45, XXREAL_0:2;

hence +infty > (lim F2) . x by XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;assume A43: x in dom (lim F2) ; :: thesis: +infty > (lim F2) . x

then reconsider x1 = x as Element of REAL ;

A44: x in A by A43, A19, MESFUNC8:def 9;

then lim (F2 # x1) = inf (F2 # x1) by A19;

then (lim F2) . x = inf (F2 # x1) by A43, MESFUNC8:def 9;

then (F2 # x1) . 0 >= (lim F2) . x by RINFSUP2:23;

then A45: (F2 . 0) . x1 >= (lim F2) . x by MESFUNC5:def 13;

upper_bound (rng (f || A)) >= (F2 . 0) . x1 by A44, A19;

then upper_bound (rng (f || A)) >= (lim F2) . x by A45, XXREAL_0:2;

hence +infty > (lim F2) . x by XXREAL_0:2, XXREAL_0:4; :: thesis: verum

-infty < (lim F2) . x

proof

( lim F2 is V171() & lim F2 is V172() )
by A42, A46, MESFUNC5:10, MESFUNC5:11;
let x be set ; :: thesis: ( x in dom (lim F2) implies -infty < (lim F2) . x )

assume A47: x in dom (lim F2) ; :: thesis: -infty < (lim F2) . x

then reconsider x1 = x as Element of REAL ;

A48: x in A by A47, A19, MESFUNC8:def 9;

then lim (F2 # x1) = inf (F2 # x1) by A19;

then (lim F2) . x = inf (F2 # x1) by A47, MESFUNC8:def 9;

then (lim F2) . x >= (f || A) . x1 by A48, A19;

then A49: (lim F2) . x >= f . x1 by A48, FUNCT_1:49;

f . x1 in REAL by A2, A48, PARTFUN1:4;

hence -infty < (lim F2) . x by A49, XXREAL_0:2, XXREAL_0:12; :: thesis: verum

end;assume A47: x in dom (lim F2) ; :: thesis: -infty < (lim F2) . x

then reconsider x1 = x as Element of REAL ;

A48: x in A by A47, A19, MESFUNC8:def 9;

then lim (F2 # x1) = inf (F2 # x1) by A19;

then (lim F2) . x = inf (F2 # x1) by A47, MESFUNC8:def 9;

then (lim F2) . x >= (f || A) . x1 by A48, A19;

then A49: (lim F2) . x >= f . x1 by A48, FUNCT_1:49;

f . x1 in REAL by A2, A48, PARTFUN1:4;

hence -infty < (lim F2) . x by A49, XXREAL_0:2, XXREAL_0:12; :: thesis: verum

then reconsider Lf2 = lim F2 as PartFunc of REAL,REAL by Th3;

A50: R_EAL Lf2 = lim F2 by MESFUNC5:def 7;

( (lim F2) - (lim F1) is V171() & (lim F2) - (lim F1) is V172() ) by A41, A42, A46, MESFUNC5:10, MESFUNC5:11, MESFUNC9:5, MESFUNC9:6;

then reconsider Lf3 = (lim F2) - (lim F1) as PartFunc of REAL,REAL by Th3;

A51: R_EAL Lf3 = (lim F2) - (lim F1) by MESFUNC5:def 7;

A52: dom (Lf2 - Lf1) = (dom (lim F2)) /\ (dom (lim F1)) by VALUED_1:12

.= dom Lf3 by A41, A46, MESFUNC5:10, MESFUNC5:17 ;

for x being Element of REAL st x in dom (Lf2 - Lf1) holds

(Lf2 - Lf1) . x = Lf3 . x

proof

then A55:
Lf2 - Lf1 = Lf3
by A52, PARTFUN1:5;
let x be Element of REAL ; :: thesis: ( x in dom (Lf2 - Lf1) implies (Lf2 - Lf1) . x = Lf3 . x )

assume A53: x in dom (Lf2 - Lf1) ; :: thesis: (Lf2 - Lf1) . x = Lf3 . x

then x in (dom (lim F2)) /\ (dom (lim F1)) by VALUED_1:12;

then A54: x in dom ((lim F2) - (lim F1)) by A41, A46, MESFUNC5:10, MESFUNC5:17;

(Lf2 - Lf1) . x = (Lf2 . x) - (Lf1 . x) by A53, VALUED_1:13;

hence (Lf2 - Lf1) . x = Lf3 . x by A54, MESFUNC1:def 4; :: thesis: verum

end;assume A53: x in dom (Lf2 - Lf1) ; :: thesis: (Lf2 - Lf1) . x = Lf3 . x

then x in (dom (lim F2)) /\ (dom (lim F1)) by VALUED_1:12;

then A54: x in dom ((lim F2) - (lim F1)) by A41, A46, MESFUNC5:10, MESFUNC5:17;

(Lf2 - Lf1) . x = (Lf2 . x) - (Lf1 . x) by A53, VALUED_1:13;

hence (Lf2 - Lf1) . x = Lf3 . x by A54, MESFUNC1:def 4; :: thesis: verum

A56: for x being Element of REAL st x in A holds

(lim F2) . x >= (f || A) . x

proof

A59:
dom |.((lim F2) - (lim F1)).| = dom ((lim F2) - (lim F1))
by MESFUNC1:def 10;
let x be Element of REAL ; :: thesis: ( x in A implies (lim F2) . x >= (f || A) . x )

assume A57: x in A ; :: thesis: (lim F2) . x >= (f || A) . x

then A58: x in dom (lim F2) by A19, MESFUNC8:def 9;

lim (F2 # x) = inf (F2 # x) by A57, A19;

then lim (F2 # x) >= (f || A) . x by A57, A19;

hence (lim F2) . x >= (f || A) . x by A58, MESFUNC8:def 9; :: thesis: verum

end;assume A57: x in A ; :: thesis: (lim F2) . x >= (f || A) . x

then A58: x in dom (lim F2) by A19, MESFUNC8:def 9;

lim (F2 # x) = inf (F2 # x) by A57, A19;

then lim (F2 # x) >= (f || A) . x by A57, A19;

hence (lim F2) . x >= (f || A) . x by A58, MESFUNC8:def 9; :: thesis: verum

A60: ( dom (lim F1) = A & dom (lim F2) = A ) by A18, A19, MESFUNC8:def 9;

A61: for x being Element of REAL st x in dom |.((lim F2) - (lim F1)).| holds

|.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x

proof

then A65:
|.((lim F2) - (lim F1)).| = R_EAL Lf3
by A51, A59, PARTFUN1:5;
let x be Element of REAL ; :: thesis: ( x in dom |.((lim F2) - (lim F1)).| implies |.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x )

assume A62: x in dom |.((lim F2) - (lim F1)).| ; :: thesis: |.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x

then A63: x in dom ((lim F2) - (lim F1)) by MESFUNC1:def 10;

then x in ((dom (lim F2)) /\ (dom (lim F1))) \ ((((lim F2) " {+infty}) /\ ((lim F1) " {+infty})) \/ (((lim F2) " {-infty}) /\ ((lim F1) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (lim F2)) /\ (dom (lim F1)) by XBOOLE_0:def 5;

then ( (lim F2) . x >= (f || A) . x & (f || A) . x >= (lim F1) . x ) by A56, A30, A60;

then A64: (lim F2) . x >= (lim F1) . x by XXREAL_0:2;

|.((lim F2) - (lim F1)).| . x = |.(((lim F2) - (lim F1)) . x).| by A62, MESFUNC1:def 10

.= |.(((lim F2) . x) - ((lim F1) . x)).| by A63, MESFUNC1:def 4

.= ((lim F2) . x) - ((lim F1) . x) by A64, EXTREAL1:def 1, XXREAL_3:40 ;

hence |.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x by A63, MESFUNC1:def 4; :: thesis: verum

end;assume A62: x in dom |.((lim F2) - (lim F1)).| ; :: thesis: |.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x

then A63: x in dom ((lim F2) - (lim F1)) by MESFUNC1:def 10;

then x in ((dom (lim F2)) /\ (dom (lim F1))) \ ((((lim F2) " {+infty}) /\ ((lim F1) " {+infty})) \/ (((lim F2) " {-infty}) /\ ((lim F1) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (lim F2)) /\ (dom (lim F1)) by XBOOLE_0:def 5;

then ( (lim F2) . x >= (f || A) . x & (f || A) . x >= (lim F1) . x ) by A56, A30, A60;

then A64: (lim F2) . x >= (lim F1) . x by XXREAL_0:2;

|.((lim F2) - (lim F1)).| . x = |.(((lim F2) - (lim F1)) . x).| by A62, MESFUNC1:def 10

.= |.(((lim F2) . x) - ((lim F1) . x)).| by A63, MESFUNC1:def 4

.= ((lim F2) . x) - ((lim F1) . x) by A64, EXTREAL1:def 1, XXREAL_3:40 ;

hence |.((lim F2) - (lim F1)).| . x = ((lim F2) - (lim F1)) . x by A63, MESFUNC1:def 4; :: thesis: verum

reconsider A2 = A as Subset of REAL ;

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

Integral (B-Meas,|.((lim F2) - (lim F1)).|) = Integral (B-Meas,((lim F2) - (lim F1))) by A61, A59, PARTFUN1:5

.= (Integral (B-Meas,((lim F2) | ((dom (lim F2)) /\ (dom (lim F1)))))) - (Integral (B-Meas,((lim F1) | ((dom (lim F2)) /\ (dom (lim F1)))))) by A18, A19, MESFUN13:17

.= (lim I2) + (- (lim I2)) by A29, A7, A18, A19, A28, A60, XXREAL_3:def 4

.= 0 by XXREAL_3:7 ;

then A66: Integral (B-Meas,Lf3) = 0 by A65, MESFUNC6:def 3;

A67: Lf2 is_integrable_on B-Meas by A19, A50, MESFUNC6:def 4;

consider ELf2 being Element of Borel_Sets such that

A68: ( ELf2 = dom (R_EAL Lf2) & R_EAL Lf2 is ELf2 -measurable ) by A19, A50, MESFUNC5:def 17;

R_EAL f = f by MESFUNC5:def 7;

then A69: (R_EAL f) | A1 = R_EAL (f | A1) by MESFUNC5:def 7;

A70: Lf2 | A1 is A1 -measurable by A1, A60, A50, A68, Th30, MEASUR12:def 11, MESFUNC6:def 1;

reconsider z = 0 as Element of REAL by XREAL_0:def 1;

A71: dom Lf3 = (dom (lim F2)) /\ (dom (lim F1)) by A41, A46, MESFUNC5:10, MESFUNC5:17;

A72: for x being Element of REAL st x in A holds

Lf2 . x >= f . x

proof

A74:
for x being Element of REAL st x in A holds
let x be Element of REAL ; :: thesis: ( x in A implies Lf2 . x >= f . x )

assume A73: x in A ; :: thesis: Lf2 . x >= f . x

then ( lim (F2 # x) = inf (F2 # x) & inf (F2 # x) >= (f || A) . x ) by A19;

then Lf2 . x >= (f || A) . x by A73, A60, MESFUNC8:def 9;

hence Lf2 . x >= f . x by A73, FUNCT_1:49; :: thesis: verum

end;assume A73: x in A ; :: thesis: Lf2 . x >= f . x

then ( lim (F2 # x) = inf (F2 # x) & inf (F2 # x) >= (f || A) . x ) by A19;

then Lf2 . x >= (f || A) . x by A73, A60, MESFUNC8:def 9;

hence Lf2 . x >= f . x by A73, FUNCT_1:49; :: thesis: verum

f . x >= Lf1 . x

proof

for x being object st x in dom Lf3 holds
let x be Element of REAL ; :: thesis: ( x in A implies f . x >= Lf1 . x )

assume A75: x in A ; :: thesis: f . x >= Lf1 . x

then ( lim (F1 # x) = sup (F1 # x) & sup (F1 # x) <= (f || A) . x ) by A18;

then Lf1 . x <= (f || A) . x by A75, A60, MESFUNC8:def 9;

hence Lf1 . x <= f . x by A75, FUNCT_1:49; :: thesis: verum

end;assume A75: x in A ; :: thesis: f . x >= Lf1 . x

then ( lim (F1 # x) = sup (F1 # x) & sup (F1 # x) <= (f || A) . x ) by A18;

then Lf1 . x <= (f || A) . x by A75, A60, MESFUNC8:def 9;

hence Lf1 . x <= f . x by A75, FUNCT_1:49; :: thesis: verum

Lf3 . x >= 0

proof

then A78:
Lf3 is nonnegative
by SUPINF_2:52;
let x be object ; :: thesis: ( x in dom Lf3 implies Lf3 . x >= 0 )

assume A76: x in dom Lf3 ; :: thesis: Lf3 . x >= 0

then reconsider x1 = x as Element of REAL ;

A77: Lf3 . x = (Lf2 . x) - (Lf1 . x) by A55, A76, VALUED_1:13;

( Lf2 . x >= f . x1 & f . x1 >= Lf1 . x ) by A72, A74, A76, A71, A60;

then Lf2 . x >= Lf1 . x by XXREAL_0:2;

hence Lf3 . x >= 0 by A77, XREAL_1:48; :: thesis: verum

end;assume A76: x in dom Lf3 ; :: thesis: Lf3 . x >= 0

then reconsider x1 = x as Element of REAL ;

A77: Lf3 . x = (Lf2 . x) - (Lf1 . x) by A55, A76, VALUED_1:13;

( Lf2 . x >= f . x1 & f . x1 >= Lf1 . x ) by A72, A74, A76, A71, A60;

then Lf2 . x >= Lf1 . x by XXREAL_0:2;

hence Lf3 . x >= 0 by A77, XREAL_1:48; :: thesis: verum

A79: R_EAL Lf3 = Lf3 by MESFUNC5:def 7;

R_EAL Lf3 is_integrable_on B-Meas by A51, A18, A19, MESFUN10:12;

then ex ELf3 being Element of Borel_Sets st

( ELf3 = dom (R_EAL Lf3) & R_EAL Lf3 is ELf3 -measurable ) by MESFUNC5:def 17;

then Lf3 is A3 -measurable by A79, A71, A60, A1, MESFUNC6:def 1;

then A80: Lf3 a.e.= (REAL --> 0) | A1, L-Meas by A1, A66, A71, A60, A78, Th25, Th29;

consider E0 being Element of L-Field such that

A82: ( L-Meas . E0 = 0 & Lf3 | (E0 `) = ((REAL --> 0) | A1) | (E0 `) ) by A80, LPSPACE1:def 10;

dom (Lf2 - f) = (dom Lf2) /\ (dom f) by VALUED_1:12;

then A81: dom (Lf2 - f) = A1 by A1, A60, A2, XBOOLE_1:28;

then A83: dom ((Lf2 - f) | (E0 `)) = A1 /\ (E0 `) by RELAT_1:61;

dom ((REAL --> 0) | A1) = (dom (REAL --> 0)) /\ A1 by RELAT_1:61;

then dom ((REAL --> 0) | A1) = A1 by XBOOLE_1:28;

then A84: dom (((REAL --> 0) | A1) | (E0 `)) = A1 /\ (E0 `) by RELAT_1:61;

for x being Element of REAL st x in dom ((Lf2 - f) | (E0 `)) holds

((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x

proof

then
(Lf2 - f) | (E0 `) = ((REAL --> 0) | A1) | (E0 `)
by A84, A81, RELAT_1:61, PARTFUN1:5;
let x be Element of REAL ; :: thesis: ( x in dom ((Lf2 - f) | (E0 `)) implies ((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x )

assume A85: x in dom ((Lf2 - f) | (E0 `)) ; :: thesis: ((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x

then A86: ( x in A1 & x in E0 ` ) by A83, XBOOLE_0:def 4;

then A87: (Lf2 . x) - (f . x) >= 0 by A72, A1, XREAL_1:48;

((Lf2 - f) | (E0 `)) . x = (Lf2 - f) . x by A85, FUNCT_1:47;

then A88: ((Lf2 - f) | (E0 `)) . x = (Lf2 . x) - (f . x) by A81, A86, VALUED_1:13;

(Lf3 | (E0 `)) . x = Lf3 . x by A85, FUNCT_1:49;

then A89: (Lf3 | (E0 `)) . x = (Lf2 . x) - (Lf1 . x) by A86, A1, A71, A60, A55, VALUED_1:13;

(((REAL --> 0) | A1) | (E0 `)) . x = ((REAL --> 0) | A1) . x by A85, FUNCT_1:49;

then (((REAL --> 0) | A1) | (E0 `)) . x = (REAL --> 0) . x by A86, FUNCT_1:49;

hence ((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x by A74, A86, A1, A88, A87, A89, A82, XREAL_1:10; :: thesis: verum

end;assume A85: x in dom ((Lf2 - f) | (E0 `)) ; :: thesis: ((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x

then A86: ( x in A1 & x in E0 ` ) by A83, XBOOLE_0:def 4;

then A87: (Lf2 . x) - (f . x) >= 0 by A72, A1, XREAL_1:48;

((Lf2 - f) | (E0 `)) . x = (Lf2 - f) . x by A85, FUNCT_1:47;

then A88: ((Lf2 - f) | (E0 `)) . x = (Lf2 . x) - (f . x) by A81, A86, VALUED_1:13;

(Lf3 | (E0 `)) . x = Lf3 . x by A85, FUNCT_1:49;

then A89: (Lf3 | (E0 `)) . x = (Lf2 . x) - (Lf1 . x) by A86, A1, A71, A60, A55, VALUED_1:13;

(((REAL --> 0) | A1) | (E0 `)) . x = ((REAL --> 0) | A1) . x by A85, FUNCT_1:49;

then (((REAL --> 0) | A1) | (E0 `)) . x = (REAL --> 0) . x by A86, FUNCT_1:49;

hence ((Lf2 - f) | (E0 `)) . x = (((REAL --> 0) | A1) | (E0 `)) . x by A74, A86, A1, A88, A87, A89, A82, XREAL_1:10; :: thesis: verum

then A90: Lf2 | A1 a.e.= f | A1, L-Meas by A81, A82, Th40, LPSPACE1:def 10;

then (R_EAL f) | A1 is A1 -measurable by A69, A1, A60, A70, Th26, MESFUNC6:def 1;

hence f is A1 -measurable by MESFUN13:19, MESFUNC6:def 1; :: thesis: ( f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )

dom (f | A1) = (dom f) /\ A1 by RELAT_1:61;

then A91: dom (f | A1) = A1 by A1, A2, XBOOLE_1:28;

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

L-Meas . A1 = diameter A by A1, MEASUR12:76;

then L-Meas . A1 = b1 - a1 by A5, A6, MEASURE5:6;

then L-Meas . A1 < +infty by XXREAL_0:9, XREAL_0:def 1;

hence f | A1 is_integrable_on L-Meas by A1, A3, A90, A60, A70, A91, Th26, Th41; :: thesis: integral (f || A) = Integral (L-Meas,(f | A))

integral (f || A) = lim I2 by A29, INTEGRA1:def 17;

then integral (f || A) = Integral (L-Meas,(lim F2)) by A19, Th38, MEASUR12:def 11, MEASUR12:def 12;

then A92: integral (f || A) = Integral (L-Meas,Lf2) by A50, MESFUNC6:def 3;

Lf2 is_integrable_on L-Meas by A67, Th48;

hence integral (f || A) = Integral (L-Meas,(f | A)) by A1, A60, A90, A91, A92, Th44; :: thesis: verum