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;
per cases ( a = b or a <> b ) ;
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;
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 )
proof
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;
defpred S1[ 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 S1[n,D]
proof
let n be Element of NAT ; :: thesis: ex D being Element of divs A st S1[n,D]
reconsider D = EqDiv (A,(2 |^ n)) as Element of divs A by INTEGRA1:def 3;
take D ; :: thesis: S1[n,D]
thus S1[n,D] ; :: thesis: verum
end;
consider T being Function of NAT,(divs A) such that
A22: for n being Element of NAT holds S1[n,T . n] from FUNCT_2:sch 3(A21);
A23: for n being Nat holds T . n = EqDiv (A,(2 |^ n))
proof
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;
A24: (f || A) | A is bounded by A3;
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
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;
then I1 = lower_sum ((f || A),T) by FUNCT_2:def 7;
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
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;
then I2 = upper_sum ((f || A),T) by FUNCT_2:def 7;
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
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;
A33: for x being set st x in dom (lim F1) holds
-infty < (lim F1) . x
proof
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;
A37: for x being set st x in dom (lim F1) holds
+infty > (lim F1) . x
proof
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;
A41: ( lim F1 is without-infty & lim F1 is without+infty ) by A33, A37, MESFUNC5:10, MESFUNC5:11;
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
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;
A46: for x being set st x in dom (lim F2) holds
-infty < (lim F2) . x
proof
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;
( lim F2 is without-infty & lim F2 is without+infty ) by A42, A46, MESFUNC5:10, MESFUNC5:11;
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 without-infty & (lim F2) - (lim F1) is without+infty ) 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
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
.= (Lf2 . x) - (Lf1 . x) ;
hence (Lf2 - Lf1) . x = Lf3 . x by A54, MESFUNC1:def 4; :: thesis: verum
end;
then A55: Lf2 - Lf1 = Lf3 by A52, PARTFUN1:5;
A56: for x being Element of REAL st x in A holds
(lim F2) . x >= (f || A) . x
proof
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;
A59: dom |.((lim F2) - (lim F1)).| = dom ((lim F2) - (lim F1)) by MESFUNC1:def 10;
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
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;
then A65: |.((lim F2) - (lim F1)).| = R_EAL Lf3 by A51, A59, PARTFUN1:5;
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
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;
A74: for x being Element of REAL st x in A holds
f . x >= Lf1 . x
proof
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;
for x being object st x in dom Lf3 holds
Lf3 . x >= 0
proof
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;
then A78: Lf3 is nonnegative by SUPINF_2:52;
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
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;
then (Lf2 - f) | (E0 `) = ((REAL --> 0) | A1) | (E0 `) by A84, A81, RELAT_1:61, PARTFUN1:5;
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;
end;