:: MESFUNC7 semantic presentation begin theorem Th1: :: MESFUNC7:1 for X being non empty set for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds f . x <= g . x ) holds g - f is nonnegative proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom f holds f . x <= g . x ) holds g - f is nonnegative let f, g be PartFunc of X,ExtREAL; ::_thesis: ( ( for x being Element of X st x in dom f holds f . x <= g . x ) implies g - f is nonnegative ) assume A1: for x being Element of X st x in dom f holds f . x <= g . x ; ::_thesis: g - f is nonnegative now__::_thesis:_for_y_being_R_eal_st_y_in_rng_(g_-_f)_holds_ 0_<=_y let y be R_eal; ::_thesis: ( y in rng (g - f) implies 0 <= y ) assume y in rng (g - f) ; ::_thesis: 0 <= y then consider x being set such that A2: x in dom (g - f) and A3: y = (g - f) . x by FUNCT_1:def_3; dom (g - f) = ((dom g) /\ (dom f)) \ (((g " {+infty}) /\ (f " {+infty})) \/ ((g " {-infty}) /\ (f " {-infty}))) by MESFUNC1:def_4; then x in (dom g) /\ (dom f) by A2, XBOOLE_0:def_5; then x in dom f by XBOOLE_0:def_4; then 0. <= (g . x) - (f . x) by A1, XXREAL_3:40; hence 0 <= y by A2, A3, MESFUNC1:def_4; ::_thesis: verum end; then rng (g - f) is nonnegative by SUPINF_2:def_9; hence g - f is nonnegative by SUPINF_2:def_16; ::_thesis: verum end; theorem Th2: :: MESFUNC7:2 for X being non empty set for Y being set for f being PartFunc of X,ExtREAL for r being Real holds (r (#) f) | Y = r (#) (f | Y) proof let X be non empty set ; ::_thesis: for Y being set for f being PartFunc of X,ExtREAL for r being Real holds (r (#) f) | Y = r (#) (f | Y) let Y be set ; ::_thesis: for f being PartFunc of X,ExtREAL for r being Real holds (r (#) f) | Y = r (#) (f | Y) let f be PartFunc of X,ExtREAL; ::_thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y) let r be Real; ::_thesis: (r (#) f) | Y = r (#) (f | Y) A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((r_(#)_f)_|_Y)_holds_ ((r_(#)_f)_|_Y)_._x_=_(r_(#)_(f_|_Y))_._x let x be Element of X; ::_thesis: ( x in dom ((r (#) f) | Y) implies ((r (#) f) | Y) . x = (r (#) (f | Y)) . x ) assume A2: x in dom ((r (#) f) | Y) ; ::_thesis: ((r (#) f) | Y) . x = (r (#) (f | Y)) . x then A3: x in (dom (r (#) f)) /\ Y by RELAT_1:61; then A4: x in Y by XBOOLE_0:def_4; A5: x in dom (r (#) f) by A3, XBOOLE_0:def_4; then x in dom f by MESFUNC1:def_6; then x in (dom f) /\ Y by A4, XBOOLE_0:def_4; then A6: x in dom (f | Y) by RELAT_1:61; then A7: x in dom (r (#) (f | Y)) by MESFUNC1:def_6; thus ((r (#) f) | Y) . x = (r (#) f) . x by A2, FUNCT_1:47 .= (R_EAL r) * (f . x) by A5, MESFUNC1:def_6 .= (R_EAL r) * ((f | Y) . x) by A6, FUNCT_1:47 .= (r (#) (f | Y)) . x by A7, MESFUNC1:def_6 ; ::_thesis: verum end; dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61 .= (dom f) /\ Y by MESFUNC1:def_6 .= dom (f | Y) by RELAT_1:61 .= dom (r (#) (f | Y)) by MESFUNC1:def_6 ; hence (r (#) f) | Y = r (#) (f | Y) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th3: :: MESFUNC7:3 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M and A3: g - f is nonnegative ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) set h = (- 1) (#) f; A4: (- 1) (#) f is_integrable_on M by A1, MESFUNC5:110; then consider E being Element of S such that A5: E = (dom ((- 1) (#) f)) /\ (dom g) and A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A2, MESFUNC5:109; A7: ex E3 being Element of S st ( E3 = dom ((- 1) (#) f) & (- 1) (#) f is_measurable_on E3 ) by A4, MESFUNC5:def_17; A8: g | E is_integrable_on M by A2, MESFUNC5:97; then A9: Integral (M,(g | E)) < +infty by MESFUNC5:96; -infty < Integral (M,(g | E)) by A8, MESFUNC5:96; then reconsider c2 = Integral (M,(g | E)) as Real by A9, XXREAL_0:14; take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) A10: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th2; g + (- f) is nonnegative by A3, MESFUNC2:8; then A11: ((- 1) (#) f) + g is nonnegative by MESFUNC2:9; A12: f | E is_integrable_on M by A1, MESFUNC5:97; then A13: Integral (M,(f | E)) < +infty by MESFUNC5:96; -infty < Integral (M,(f | E)) by A12, MESFUNC5:96; then reconsider c1 = Integral (M,(f | E)) as Real by A13, XXREAL_0:14; A14: (R_EAL (- 1)) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1; ex E2 being Element of S st ( E2 = dom g & g is_measurable_on E2 ) by A2, MESFUNC5:def_17; then ex A being Element of S st ( A = dom (((- 1) (#) f) + g) & ((- 1) (#) f) + g is_measurable_on A ) by A7, MESFUNC5:47; then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A6, A11, MESFUNC5:90; then 0 <= ((R_EAL (- 1)) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A12, A10, MESFUNC5:110; then 0 <= (- c1) + c2 by A14, SUPINF_2:1; then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6; hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, MESFUNC1:def_6; ::_thesis: verum end; begin registration let X be non empty set ; cluster Relation-like X -defined ExtREAL -valued V18() extreal-yielding nonnegative for Element of K6(K7(X,ExtREAL)); existence ex b1 being PartFunc of X,ExtREAL st b1 is nonnegative proof set f = the PartFunc of X,ExtREAL; take |. the PartFunc of X,ExtREAL.| ; ::_thesis: |. the PartFunc of X,ExtREAL.| is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_|._the_PartFunc_of_X,ExtREAL.|_holds_ 0._<=_|._the_PartFunc_of_X,ExtREAL.|_._x let x be set ; ::_thesis: ( x in dom |. the PartFunc of X,ExtREAL.| implies 0. <= |. the PartFunc of X,ExtREAL.| . x ) assume x in dom |. the PartFunc of X,ExtREAL.| ; ::_thesis: 0. <= |. the PartFunc of X,ExtREAL.| . x then |. the PartFunc of X,ExtREAL.| . x = |.( the PartFunc of X,ExtREAL . x).| by MESFUNC1:def_10; hence 0. <= |. the PartFunc of X,ExtREAL.| . x by EXTREAL2:3; ::_thesis: verum end; hence |. the PartFunc of X,ExtREAL.| is nonnegative by SUPINF_2:52; ::_thesis: verum end; end; registration let X be non empty set ; let f be PartFunc of X,ExtREAL; cluster|.f.| -> nonnegative for PartFunc of X,ExtREAL; correctness coherence for b1 being PartFunc of X,ExtREAL st b1 = |.f.| holds b1 is nonnegative ; proof now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_ 0._<=_|.f.|_._x let x be set ; ::_thesis: ( x in dom |.f.| implies 0. <= |.f.| . x ) assume x in dom |.f.| ; ::_thesis: 0. <= |.f.| . x then |.f.| . x = |.(f . x).| by MESFUNC1:def_10; hence 0. <= |.f.| . x by EXTREAL2:3; ::_thesis: verum end; hence for b1 being PartFunc of X,ExtREAL st b1 = |.f.| holds b1 is nonnegative by SUPINF_2:52; ::_thesis: verum end; end; theorem :: MESFUNC7:4 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M implies ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) ) assume A1: f is_integrable_on M ; ::_thesis: ex F being Function of NAT,S st ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) then consider E being Element of S such that A2: E = dom f and A3: f is_measurable_on E by MESFUNC5:def_17; defpred S1[ Element of NAT , set ] means $2 = E /\ (great_eq_dom (|.f.|,(R_EAL (1 / ($1 + 1))))); A4: dom |.f.| = E by A2, MESFUNC1:def_10; now__::_thesis:_for_x_being_set_st_x_in_E_\_(eq_dom_(f,0.))_holds_ x_in_E_/\_(great_dom_(|.f.|,0.)) let x be set ; ::_thesis: ( x in E \ (eq_dom (f,0.)) implies x in E /\ (great_dom (|.f.|,0.)) ) assume A5: x in E \ (eq_dom (f,0.)) ; ::_thesis: x in E /\ (great_dom (|.f.|,0.)) then reconsider z = x as Element of X ; reconsider y = f . z as R_eal ; A6: x in E by A5, XBOOLE_0:def_5; then A7: x in dom |.f.| by A2, MESFUNC1:def_10; not x in eq_dom (f,0.) by A5, XBOOLE_0:def_5; then not y = 0. by A2, A6, MESFUNC1:def_15; then 0. < |.(f . z).| by EXTREAL2:4; then 0. < |.f.| . z by A7, MESFUNC1:def_10; then x in great_dom (|.f.|,0.) by A7, MESFUNC1:def_13; hence x in E /\ (great_dom (|.f.|,0.)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A8: E \ (eq_dom (f,0.)) c= E /\ (great_dom (|.f.|,0.)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_E_/\_(great_dom_(|.f.|,0.))_holds_ x_in_E_\_(eq_dom_(f,0.)) let x be set ; ::_thesis: ( x in E /\ (great_dom (|.f.|,0.)) implies x in E \ (eq_dom (f,0.)) ) assume A9: x in E /\ (great_dom (|.f.|,0.)) ; ::_thesis: x in E \ (eq_dom (f,0.)) then reconsider z = x as Element of X ; x in great_dom (|.f.|,0.) by A9, XBOOLE_0:def_4; then A10: 0. < |.f.| . z by MESFUNC1:def_13; A11: x in E by A9, XBOOLE_0:def_4; then x in dom |.f.| by A2, MESFUNC1:def_10; then A12: 0. < |.(f . z).| by A10, MESFUNC1:def_10; not x in eq_dom (f,0.) proof assume x in eq_dom (f,0.) ; ::_thesis: contradiction then f . z = 0. by MESFUNC1:def_15; hence contradiction by A12, EXTREAL2:5; ::_thesis: verum end; hence x in E \ (eq_dom (f,0.)) by A11, XBOOLE_0:def_5; ::_thesis: verum end; then A13: E /\ (great_dom (|.f.|,0.)) c= E \ (eq_dom (f,0.)) by TARSKI:def_3; A14: |.f.| is_measurable_on E by A2, A3, MESFUNC2:27; A15: for n being Element of NAT ex Z being Element of S st S1[n,Z] proof let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z] take E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ; ::_thesis: ( E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))))] ) thus ( E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))))] ) by A14, A4, MESFUNC1:27; ::_thesis: verum end; consider F being Function of NAT,S such that A16: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A15); A17: for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) proof let n be Element of NAT ; ::_thesis: ( F . n in S & M . (F . n) < +infty ) set d = R_EAL (1 / (n + 1)); set En = F . n; set g = |.f.| | (F . n); A18: |.f.| | (F . n) is nonnegative by MESFUNC5:15; set z = R_EAL (1 / (n + 1)); A19: |.f.| | E = |.f.| by A4, RELAT_1:69; A20: F . n = E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) by A16; then A21: dom (|.f.| | (F . n)) = F . n by A4, RELAT_1:62, XBOOLE_1:17; (dom |.f.|) /\ (F . n) = E /\ (F . n) by A2, MESFUNC1:def_10; then A22: (dom |.f.|) /\ (F . n) = F . n by A20, XBOOLE_1:17, XBOOLE_1:28; |.f.| is_measurable_on F . n by A14, A20, MESFUNC1:30, XBOOLE_1:17; then A23: |.f.| | (F . n) is_measurable_on F . n by A22, MESFUNC5:42; then A24: integral+ (M,(|.f.| | (F . n))) = Integral (M,(|.f.| | (F . n))) by A21, MESFUNC5:15, MESFUNC5:88; |.f.| is_integrable_on M by A1, A2, A3, MESFUNC5:100; then A25: Integral (M,|.f.|) < +infty by MESFUNC5:96; A26: ((R_EAL (1 / (n + 1))) * (M . (F . n))) / (R_EAL (1 / (n + 1))) = M . (F . n) by XXREAL_3:88; F . n c= E by A20, XBOOLE_1:17; then A27: Integral (M,(|.f.| | (F . n))) <= Integral (M,|.f.|) by A2, A3, A4, A19, MESFUNC2:27, MESFUNC5:93; consider nf being PartFunc of X,ExtREAL such that A28: nf is_simple_func_in S and A29: dom nf = F . n and A30: for x being set st x in F . n holds nf . x = R_EAL (1 / (n + 1)) by MESFUNC5:41; for x being set st x in dom nf holds nf . x >= 0 by A29, A30; then A31: nf is nonnegative by SUPINF_2:52; then A32: Integral (M,nf) = integral' (M,nf) by A28, MESFUNC5:89; A33: F . n c= great_eq_dom (|.f.|,(R_EAL (1 / (n + 1)))) by A20, XBOOLE_1:17; A34: for x being Element of X st x in dom nf holds nf . x <= (|.f.| | (F . n)) . x proof let x be Element of X; ::_thesis: ( x in dom nf implies nf . x <= (|.f.| | (F . n)) . x ) assume A35: x in dom nf ; ::_thesis: nf . x <= (|.f.| | (F . n)) . x then A36: R_EAL (1 / (n + 1)) <= |.f.| . x by A33, A29, MESFUNC1:def_14; (|.f.| | (F . n)) . x = |.f.| . x by A21, A29, A35, FUNCT_1:47; hence nf . x <= (|.f.| | (F . n)) . x by A29, A30, A35, A36; ::_thesis: verum end; nf is_measurable_on F . n by A28, MESFUNC2:34; then integral+ (M,nf) <= integral+ (M,(|.f.| | (F . n))) by A21, A23, A18, A29, A31, A34, MESFUNC5:85; then A37: integral+ (M,nf) <= Integral (M,|.f.|) by A24, A27, XXREAL_0:2; A38: +infty / (R_EAL (1 / (n + 1))) = +infty by XXREAL_3:83; integral+ (M,nf) = Integral (M,nf) by A28, A31, MESFUNC5:89; then integral+ (M,nf) = (R_EAL (1 / (n + 1))) * (M . (F . n)) by A29, A30, A32, MESFUNC5:104; then (R_EAL (1 / (n + 1))) * (M . (F . n)) < +infty by A25, A37, XXREAL_0:2; hence ( F . n in S & M . (F . n) < +infty ) by A26, A38, XXREAL_3:80; ::_thesis: verum end; take F ; ::_thesis: ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) for n being Element of NAT holds F . n = E /\ (great_eq_dom (|.f.|,(R_EAL (0 + (1 / (n + 1)))))) by A16; then E /\ (great_dom (|.f.|,(R_EAL 0))) = union (rng F) by MESFUNC1:22; hence ( ( for n being Element of NAT holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (f,0.)) = union (rng F) & ( for n being Element of NAT holds ( F . n in S & M . (F . n) < +infty ) ) ) by A2, A16, A13, A8, A17, XBOOLE_0:def_10; ::_thesis: verum end; begin notation let F be Relation; synonym extreal-yielding F for ext-real-valued ; end; registration cluster Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like extreal-yielding for set ; existence ex b1 being FinSequence st b1 is extreal-yielding proof set f = the FinSequence of ExtREAL ; the FinSequence of ExtREAL is extreal-yielding ; hence ex b1 being FinSequence st b1 is extreal-yielding ; ::_thesis: verum end; end; definition func multextreal -> BinOp of ExtREAL means :Def1: :: MESFUNC7:def 1 for x, y being Element of ExtREAL holds it . (x,y) = x * y; existence ex b1 being BinOp of ExtREAL st for x, y being Element of ExtREAL holds b1 . (x,y) = x * y from BINOP_1:sch_4(); uniqueness for b1, b2 being BinOp of ExtREAL st ( for x, y being Element of ExtREAL holds b1 . (x,y) = x * y ) & ( for x, y being Element of ExtREAL holds b2 . (x,y) = x * y ) holds b1 = b2 from BINOP_2:sch_2(); end; :: deftheorem Def1 defines multextreal MESFUNC7:def_1_:_ for b1 being BinOp of ExtREAL holds ( b1 = multextreal iff for x, y being Element of ExtREAL holds b1 . (x,y) = x * y ); registration cluster multextreal -> commutative associative ; coherence ( multextreal is commutative & multextreal is associative ) proof A1: for a, b, c being Element of ExtREAL holds multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c) proof let a, b, c be Element of ExtREAL ; ::_thesis: multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c) multextreal . (a,(multextreal . (b,c))) = multextreal . (a,(b * c)) by Def1; then multextreal . (a,(multextreal . (b,c))) = a * (b * c) by Def1; then multextreal . (a,(multextreal . (b,c))) = (a * b) * c by XXREAL_3:66; then multextreal . (a,(multextreal . (b,c))) = multextreal . ((a * b),c) by Def1; hence multextreal . (a,(multextreal . (b,c))) = multextreal . ((multextreal . (a,b)),c) by Def1; ::_thesis: verum end; for a, b being Element of ExtREAL holds multextreal . (a,b) = multextreal . (b,a) proof let a, b be Element of ExtREAL ; ::_thesis: multextreal . (a,b) = multextreal . (b,a) multextreal . (a,b) = a * b by Def1; hence multextreal . (a,b) = multextreal . (b,a) by Def1; ::_thesis: verum end; hence ( multextreal is commutative & multextreal is associative ) by A1, BINOP_1:def_2, BINOP_1:def_3; ::_thesis: verum end; end; Lm1: 1. is_a_unity_wrt multextreal proof for r being Element of ExtREAL holds multextreal . (r,1.) = r proof let r be Element of ExtREAL ; ::_thesis: multextreal . (r,1.) = r multextreal . (r,1.) = r * 1. by Def1; hence multextreal . (r,1.) = r by XXREAL_3:81; ::_thesis: verum end; then A1: 1. is_a_right_unity_wrt multextreal by BINOP_1:def_6; for r being Element of ExtREAL holds multextreal . (1.,r) = r proof let r be Element of ExtREAL ; ::_thesis: multextreal . (1.,r) = r multextreal . (1.,r) = 1. * r by Def1; hence multextreal . (1.,r) = r by XXREAL_3:81; ::_thesis: verum end; then 1. is_a_left_unity_wrt multextreal by BINOP_1:def_5; hence 1. is_a_unity_wrt multextreal by A1, BINOP_1:def_7; ::_thesis: verum end; theorem Th5: :: MESFUNC7:5 the_unity_wrt multextreal = 1 by Lm1, BINOP_1:def_8; registration cluster multextreal -> having_a_unity ; coherence multextreal is having_a_unity by Lm1, Th5, SETWISEO:14; end; definition let F be extreal-yielding FinSequence; func Product F -> Element of ExtREAL means :Def2: :: MESFUNC7:def 2 ex f being FinSequence of ExtREAL st ( f = F & it = multextreal $$ f ); existence ex b1 being Element of ExtREAL ex f being FinSequence of ExtREAL st ( f = F & b1 = multextreal $$ f ) proof rng F c= ExtREAL by VALUED_0:def_2; then reconsider f = F as FinSequence of ExtREAL by FINSEQ_1:def_4; take multextreal $$ f ; ::_thesis: ex f being FinSequence of ExtREAL st ( f = F & multextreal $$ f = multextreal $$ f ) thus ex f being FinSequence of ExtREAL st ( f = F & multextreal $$ f = multextreal $$ f ) ; ::_thesis: verum end; uniqueness for b1, b2 being Element of ExtREAL st ex f being FinSequence of ExtREAL st ( f = F & b1 = multextreal $$ f ) & ex f being FinSequence of ExtREAL st ( f = F & b2 = multextreal $$ f ) holds b1 = b2 ; end; :: deftheorem Def2 defines Product MESFUNC7:def_2_:_ for F being extreal-yielding FinSequence for b2 being Element of ExtREAL holds ( b2 = Product F iff ex f being FinSequence of ExtREAL st ( f = F & b2 = multextreal $$ f ) ); registration let x be Element of ExtREAL ; let n be Nat; clustern |-> x -> extreal-yielding ; coherence n |-> x is extreal-yielding ; end; definition let x be Element of ExtREAL ; let k be Nat; funcx |^ k -> set equals :: MESFUNC7:def 3 Product (k |-> x); coherence Product (k |-> x) is set ; end; :: deftheorem defines |^ MESFUNC7:def_3_:_ for x being Element of ExtREAL for k being Nat holds x |^ k = Product (k |-> x); definition let x be Element of ExtREAL ; let k be Nat; :: original: |^ redefine funcx |^ k -> R_eal; coherence x |^ k is R_eal ; end; registration cluster <*> ExtREAL -> extreal-yielding ; coherence <*> ExtREAL is extreal-yielding ; end; registration let r be Element of ExtREAL ; cluster<*r*> -> extreal-yielding ; coherence <*r*> is extreal-yielding ; end; theorem Th6: :: MESFUNC7:6 Product (<*> ExtREAL) = 1 proof Product (<*> ExtREAL) = multextreal $$ (<*> ExtREAL) by Def2; hence Product (<*> ExtREAL) = 1 by Th5, FINSOP_1:10; ::_thesis: verum end; theorem Th7: :: MESFUNC7:7 for r being Element of ExtREAL holds Product <*r*> = r proof let r be Element of ExtREAL ; ::_thesis: Product <*r*> = r reconsider r9 = r as Element of ExtREAL ; reconsider F = <*r9*> as FinSequence of ExtREAL ; multextreal $$ F = r by FINSOP_1:11; hence Product <*r*> = r by Def2; ::_thesis: verum end; registration let f, g be extreal-yielding FinSequence; clusterf ^ g -> extreal-yielding ; coherence f ^ g is extreal-yielding proof A1: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31; A2: rng g c= ExtREAL by VALUED_0:def_2; rng f c= ExtREAL by VALUED_0:def_2; then rng (f ^ g) c= ExtREAL by A2, A1, XBOOLE_1:8; hence f ^ g is extreal-yielding by VALUED_0:def_2; ::_thesis: verum end; end; theorem Th8: :: MESFUNC7:8 for F being extreal-yielding FinSequence for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r proof let F be extreal-yielding FinSequence; ::_thesis: for r being Element of ExtREAL holds Product (F ^ <*r*>) = (Product F) * r let r be Element of ExtREAL ; ::_thesis: Product (F ^ <*r*>) = (Product F) * r A1: rng (F ^ <*r*>) c= ExtREAL by VALUED_0:def_2; rng F c= ExtREAL by VALUED_0:def_2; then reconsider Fr = F ^ <*r*>, Ff = F as FinSequence of ExtREAL by A1, FINSEQ_1:def_4; reconsider Ff1 = Ff as extreal-yielding FinSequence ; Product (F ^ <*r*>) = multextreal $$ Fr by Def2; then Product (F ^ <*r*>) = multextreal . ((multextreal $$ Ff),r) by FINSOP_1:4; then Product (F ^ <*r*>) = multextreal . ((Product Ff1),r) by Def2; hence Product (F ^ <*r*>) = (Product F) * r by Def1; ::_thesis: verum end; theorem Th9: :: MESFUNC7:9 for x being Element of ExtREAL holds x |^ 1 = x proof let x be Element of ExtREAL ; ::_thesis: x |^ 1 = x Product (1 |-> x) = Product <*x*> by FINSEQ_2:59; hence x |^ 1 = x by Th7; ::_thesis: verum end; theorem Th10: :: MESFUNC7:10 for x being Element of ExtREAL for k being Nat holds x |^ (k + 1) = (x |^ k) * x proof let x be Element of ExtREAL ; ::_thesis: for k being Nat holds x |^ (k + 1) = (x |^ k) * x defpred S1[ Nat] means x |^ ($1 + 1) = (x |^ $1) * x; A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume x |^ (k + 1) = (x |^ k) * x ; ::_thesis: S1[k + 1] reconsider k1 = k + 1 as Element of NAT ; Product ((k1 + 1) |-> x) = Product ((k1 |-> x) ^ <*x*>) by FINSEQ_2:60; hence S1[k + 1] by Th8; ::_thesis: verum end; x |^ (0 + 1) = Product <*x*> by FINSEQ_2:59; then x |^ (0 + 1) = x by Th7; then x |^ (0 + 1) = 1. * x by XXREAL_3:81; then A2: S1[ 0 ] by Th6, FINSEQ_2:58; for k being Nat holds S1[k] from NAT_1:sch_2(A2, A1); hence for k being Nat holds x |^ (k + 1) = (x |^ k) * x ; ::_thesis: verum end; definition let k be Nat; let X be non empty set ; let f be PartFunc of X,ExtREAL; funcf |^ k -> PartFunc of X,ExtREAL means :Def4: :: MESFUNC7:def 4 ( dom it = dom f & ( for x being Element of X st x in dom it holds it . x = (f . x) |^ k ) ); existence ex b1 being PartFunc of X,ExtREAL st ( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds b1 . x = (f . x) |^ k ) ) proof deffunc H1( set ) -> R_eal = (f . $1) |^ k; defpred S1[ set ] means $1 in dom f; consider f3 being PartFunc of X,ExtREAL such that A1: for d being Element of X holds ( d in dom f3 iff S1[d] ) and A2: for d being Element of X st d in dom f3 holds f3 /. d = H1(d) from PARTFUN2:sch_2(); take f3 ; ::_thesis: ( dom f3 = dom f & ( for x being Element of X st x in dom f3 holds f3 . x = (f . x) |^ k ) ) for x being set st x in dom f holds x in dom f3 by A1; then A3: dom f c= dom f3 by TARSKI:def_3; for x being set st x in dom f3 holds x in dom f by A1; then dom f3 c= dom f by TARSKI:def_3; hence dom f3 = dom f by A3, XBOOLE_0:def_10; ::_thesis: for x being Element of X st x in dom f3 holds f3 . x = (f . x) |^ k let d be Element of X; ::_thesis: ( d in dom f3 implies f3 . d = (f . d) |^ k ) assume A4: d in dom f3 ; ::_thesis: f3 . d = (f . d) |^ k then f3 /. d = (f . d) |^ k by A2; hence f3 . d = (f . d) |^ k by A4, PARTFUN1:def_6; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds b1 . x = (f . x) |^ k ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds b2 . x = (f . x) |^ k ) holds b1 = b2 proof let f1, f2 be PartFunc of X,ExtREAL; ::_thesis: ( dom f1 = dom f & ( for x being Element of X st x in dom f1 holds f1 . x = (f . x) |^ k ) & dom f2 = dom f & ( for x being Element of X st x in dom f2 holds f2 . x = (f . x) |^ k ) implies f1 = f2 ) assume that A5: dom f1 = dom f and A6: for d being Element of X st d in dom f1 holds f1 . d = (f . d) |^ k and A7: dom f2 = dom f and A8: for d being Element of X st d in dom f2 holds f2 . d = (f . d) |^ k ; ::_thesis: f1 = f2 for d being Element of X st d in dom f holds f1 . d = f2 . d proof let d be Element of X; ::_thesis: ( d in dom f implies f1 . d = f2 . d ) assume A9: d in dom f ; ::_thesis: f1 . d = f2 . d then f1 . d = (f . d) |^ k by A5, A6; hence f1 . d = f2 . d by A7, A8, A9; ::_thesis: verum end; hence f1 = f2 by A5, A7, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def4 defines |^ MESFUNC7:def_4_:_ for k being Nat for X being non empty set for f, b4 being PartFunc of X,ExtREAL holds ( b4 = f |^ k iff ( dom b4 = dom f & ( for x being Element of X st x in dom b4 holds b4 . x = (f . x) |^ k ) ) ); theorem Th11: :: MESFUNC7:11 for x being Element of ExtREAL for y being real number for k being Nat st x = y holds x |^ k = y |^ k proof let x be Element of ExtREAL ; ::_thesis: for y being real number for k being Nat st x = y holds x |^ k = y |^ k let y be real number ; ::_thesis: for k being Nat st x = y holds x |^ k = y |^ k let k be Nat; ::_thesis: ( x = y implies x |^ k = y |^ k ) defpred S1[ Nat] means x |^ $1 = y |^ $1; assume A1: x = y ; ::_thesis: x |^ k = y |^ k A2: for k being Nat st S1[k] holds S1[k + 1] proof reconsider y1 = y as Element of REAL by XREAL_0:def_1; let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then (x |^ k) * x = (y1 |^ k) * y1 by A1, EXTREAL1:1; then (x |^ k) * x = y |^ (k + 1) by NEWTON:6; hence S1[k + 1] by Th10; ::_thesis: verum end; x |^ 0 = 1. by Th6, FINSEQ_2:58; then A3: S1[ 0 ] by NEWTON:4; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A2); hence x |^ k = y |^ k ; ::_thesis: verum end; theorem Th12: :: MESFUNC7:12 for x being Element of ExtREAL for k being Nat st 0 <= x holds 0 <= x |^ k proof let x be Element of ExtREAL ; ::_thesis: for k being Nat st 0 <= x holds 0 <= x |^ k let k be Nat; ::_thesis: ( 0 <= x implies 0 <= x |^ k ) defpred S1[ Nat] means 0 <= x |^ $1; assume A1: 0 <= x ; ::_thesis: 0 <= x |^ k A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] x |^ (k + 1) = (x |^ k) * x by Th10; hence S1[k + 1] by A1, A3; ::_thesis: verum end; A4: S1[ 0 ] by Th6, FINSEQ_2:58; for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2); hence 0 <= x |^ k ; ::_thesis: verum end; theorem Th13: :: MESFUNC7:13 for k being Nat st 1 <= k holds +infty |^ k = +infty proof defpred S1[ Nat] means +infty |^ $1 = +infty ; A1: for k being non empty Nat st S1[k] holds S1[k + 1] proof let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] +infty |^ (k + 1) = (+infty |^ k) * +infty by Th10; hence S1[k + 1] by A2, XXREAL_3:def_5; ::_thesis: verum end; A3: S1[1] by Th9; for k being non empty Nat holds S1[k] from NAT_1:sch_10(A3, A1); hence for k being Nat st 1 <= k holds +infty |^ k = +infty ; ::_thesis: verum end; theorem Th14: :: MESFUNC7:14 for k being Nat for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for E being Element of S st E c= dom f & f is_measurable_on E holds |.f.| |^ k is_measurable_on E proof let k be Nat; ::_thesis: for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for E being Element of S st E c= dom f & f is_measurable_on E holds |.f.| |^ k is_measurable_on E let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for E being Element of S st E c= dom f & f is_measurable_on E holds |.f.| |^ k is_measurable_on E let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for E being Element of S st E c= dom f & f is_measurable_on E holds |.f.| |^ k is_measurable_on E let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st E c= dom f & f is_measurable_on E holds |.f.| |^ k is_measurable_on E let E be Element of S; ::_thesis: ( E c= dom f & f is_measurable_on E implies |.f.| |^ k is_measurable_on E ) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; assume that A1: E c= dom f and A2: f is_measurable_on E ; ::_thesis: |.f.| |^ k is_measurable_on E A3: dom (|.f.| |^ k) = dom |.f.| by Def4; then A4: dom (|.f.| |^ k) = dom f by MESFUNC1:def_10; percases ( k = 0 or k <> 0 ) ; supposeA5: k = 0 ; ::_thesis: |.f.| |^ k is_measurable_on E A6: for r being real number st 1 < r holds E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S proof let r be real number ; ::_thesis: ( 1 < r implies E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S ) assume A7: 1 < r ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S E c= less_dom ((|.f.| |^ k),(R_EAL r)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in less_dom ((|.f.| |^ k),(R_EAL r)) ) assume A8: x in E ; ::_thesis: x in less_dom ((|.f.| |^ k),(R_EAL r)) then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def4; then (|.f.| |^ k) . x < r by A5, A7, Th6, FINSEQ_2:58; hence x in less_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A8, MESFUNC1:def_11; ::_thesis: verum end; then E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) = E by XBOOLE_1:28; hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S ; ::_thesis: verum end; A9: E c= dom (|.f.| |^ k) by A1, A3, MESFUNC1:def_10; for r being real number holds E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S proof let r be real number ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S now__::_thesis:_(_r_<=_1_implies_E_/\_(less_dom_((|.f.|_|^_k),(R_EAL_r)))_in_S_) assume A10: r <= 1 ; ::_thesis: E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S E c= great_eq_dom ((|.f.| |^ k),(R_EAL r)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) ) assume A11: x in E ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) then (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, Def4; then r <= (|.f.| |^ k) . x by A5, A10, Th6, FINSEQ_2:58; hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A11, MESFUNC1:def_14; ::_thesis: verum end; then E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) = E by XBOOLE_1:28; then E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) = E \ E by A9, MESFUNC1:17; hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S ; ::_thesis: verum end; hence E /\ (less_dom ((|.f.| |^ k),(R_EAL r))) in S by A6; ::_thesis: verum end; hence |.f.| |^ k is_measurable_on E by MESFUNC1:def_16; ::_thesis: verum end; supposeA12: k <> 0 ; ::_thesis: |.f.| |^ k is_measurable_on E then A13: (1 / k) * k = 1 by XCMPLX_1:87; A14: for r being real number st 0 < r holds great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) proof let r be real number ; ::_thesis: ( 0 < r implies great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) ) assume A15: 0 < r ; ::_thesis: great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) A16: great_eq_dom ((|.f.| |^ k),(R_EAL r)) c= great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) or x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) ) assume A17: x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) then A18: x in dom (|.f.| |^ k) by MESFUNC1:def_14; then A19: |.f.| . x = |.(f . x).| by A3, MESFUNC1:def_10; then A20: 0 <= |.f.| . x by EXTREAL2:3; percases ( |.f.| . x = +infty or |.f.| . x <> +infty ) ; suppose |.f.| . x = +infty ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) then R_EAL (r to_power (1 / k)) <= |.f.| . x by XXREAL_0:3; hence x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) by A3, A18, MESFUNC1:def_14; ::_thesis: verum end; suppose |.f.| . x <> +infty ; ::_thesis: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) then reconsider fx = |.f.| . x as Element of REAL by A20, XXREAL_0:14; A21: r <= (|.f.| |^ k) . x by A17, MESFUNC1:def_14; (|.f.| |^ k) . x = (|.f.| . x) |^ k by A18, Def4; then A22: r <= fx to_power k1 by A21, Th11; (fx to_power k) to_power (1 / k) = fx to_power ((k * 1) / k) by A12, A19, EXTREAL2:3, HOLDER_1:2; then A23: (fx to_power k) to_power (1 / k) = fx by A13, POWER:25; r is Real by XREAL_0:def_1; then r to_power (1 / k) <= (fx to_power k) to_power (1 / k) by A12, A15, A22, HOLDER_1:3; hence x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) by A3, A18, A23, MESFUNC1:def_14; ::_thesis: verum end; end; end; great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) c= great_eq_dom ((|.f.| |^ k),(R_EAL r)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) ) assume A24: x in great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) then A25: x in dom |.f.| by MESFUNC1:def_14; then A26: (|.f.| |^ k) . x = (|.f.| . x) |^ k by A3, Def4; |.f.| . x = |.(f . x).| by A25, MESFUNC1:def_10; then A27: 0 <= |.f.| . x by EXTREAL2:3; A28: now__::_thesis:_(_|.f.|_._x_<>_+infty_implies_r_<=_(|.f.|_|^_k)_._x_) assume |.f.| . x <> +infty ; ::_thesis: r <= (|.f.| |^ k) . x then reconsider fx = |.f.| . x as Element of REAL by A27, XXREAL_0:14; reconsider R = r to_power (1 / k) as Real by XREAL_0:def_1; A29: 0 < r to_power (1 / k) by A15, POWER:34; A30: R to_power k1 = r to_power ((1 / k) * k) by A15, POWER:33; A31: (|.f.| |^ k) . x = fx |^ k by A26, Th11; R_EAL (r to_power (1 / k)) <= |.f.| . x by A24, MESFUNC1:def_14; then r to_power 1 <= fx to_power k by A12, A13, A29, A30, HOLDER_1:3; hence r <= (|.f.| |^ k) . x by A31, POWER:25; ::_thesis: verum end; now__::_thesis:_(_|.f.|_._x_=_+infty_implies_r_<=_(|.f.|_|^_k)_._x_) assume |.f.| . x = +infty ; ::_thesis: r <= (|.f.| |^ k) . x then (|.f.| . x) |^ k = +infty by A12, Th13, NAT_1:14; hence r <= (|.f.| |^ k) . x by A26, XXREAL_0:3; ::_thesis: verum end; hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A3, A25, A28, MESFUNC1:def_14; ::_thesis: verum end; hence great_eq_dom ((|.f.| |^ k),(R_EAL r)) = great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k)))) by A16, XBOOLE_0:def_10; ::_thesis: verum end; A32: |.f.| is_measurable_on E by A1, A2, MESFUNC2:27; for r being real number holds E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S proof let r be real number ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S percases ( r <= 0 or 0 < r ) ; supposeA33: r <= 0 ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S E c= great_eq_dom ((|.f.| |^ k),(R_EAL r)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in E or x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) ) assume A34: x in E ; ::_thesis: x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) then A35: |.f.| . x = |.(f . x).| by A1, A3, A4, MESFUNC1:def_10; (|.f.| |^ k) . x = (|.f.| . x) |^ k by A1, A4, A34, Def4; then r <= (|.f.| |^ k) . x by A33, A35, Th12, EXTREAL2:3; hence x in great_eq_dom ((|.f.| |^ k),(R_EAL r)) by A1, A4, A34, MESFUNC1:def_14; ::_thesis: verum end; then E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) = E by XBOOLE_1:28; hence E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S ; ::_thesis: verum end; suppose 0 < r ; ::_thesis: E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S then E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) = E /\ (great_eq_dom (|.f.|,(R_EAL (r to_power (1 / k))))) by A14; hence E /\ (great_eq_dom ((|.f.| |^ k),(R_EAL r))) in S by A1, A3, A4, A32, MESFUNC1:27; ::_thesis: verum end; end; end; hence |.f.| |^ k is_measurable_on E by A1, A4, MESFUNC1:27; ::_thesis: verum end; end; end; theorem Th15: :: MESFUNC7:15 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let f, g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let E be Element of S; ::_thesis: ( (dom f) /\ (dom g) = E & f is V67() & g is V67() & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E ) assume that A1: (dom f) /\ (dom g) = E and A2: f is V67() and A3: g is V67() and A4: f is_measurable_on E and A5: g is_measurable_on E ; ::_thesis: f (#) g is_measurable_on E A6: dom (f (#) g) = (dom f) /\ (dom g) by MESFUNC1:def_5; A7: dom ((1 / 4) (#) (|.(f + g).| |^ 2)) = dom (|.(f + g).| |^ 2) by MESFUNC1:def_6; A8: dom (|.(f - g).| |^ 2) = dom |.(f - g).| by Def4; then A9: dom (|.(f - g).| |^ 2) = dom (f - g) by MESFUNC1:def_10; then A10: dom (|.(f - g).| |^ 2) = (dom f) /\ (dom g) by A2, MESFUNC2:2; then A11: dom (|.(f - g).| |^ 2) c= dom g by XBOOLE_1:17; A12: dom ((1 / 4) (#) (|.(f - g).| |^ 2)) = dom (|.(f - g).| |^ 2) by MESFUNC1:def_6; A13: dom (|.(f + g).| |^ 2) = dom |.(f + g).| by Def4; then A14: dom (|.(f + g).| |^ 2) = dom (f + g) by MESFUNC1:def_10; then A15: dom (|.(f + g).| |^ 2) = (dom f) /\ (dom g) by A2, MESFUNC2:2; then A16: dom (|.(f + g).| |^ 2) c= dom g by XBOOLE_1:17; A17: dom (|.(f + g).| |^ 2) c= dom f by A15, XBOOLE_1:17; for x being Element of X st x in dom (|.(f + g).| |^ 2) holds |.((|.(f + g).| |^ 2) . x).| < +infty proof let x be Element of X; ::_thesis: ( x in dom (|.(f + g).| |^ 2) implies |.((|.(f + g).| |^ 2) . x).| < +infty ) assume A18: x in dom (|.(f + g).| |^ 2) ; ::_thesis: |.((|.(f + g).| |^ 2) . x).| < +infty then A19: |.(g . x).| < +infty by A3, A16, MESFUNC2:def_1; |.(f . x).| < +infty by A2, A17, A18, MESFUNC2:def_1; then reconsider c1 = f . x, c2 = g . x as Real by A19, EXTREAL2:30; (f . x) + (g . x) = c1 + c2 by SUPINF_2:1; then |.((f . x) + (g . x)).| = abs (c1 + c2) by EXTREAL2:1; then A20: |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2)) by EXTREAL1:1; (|.(f + g).| |^ 2) . x = (|.(f + g).| . x) |^ (1 + 1) by A18, Def4; then A21: (|.(f + g).| |^ 2) . x = ((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x) by Th10; A22: |.((f + g) . x).| = |.((f . x) + (g . x)).| by A14, A18, MESFUNC1:def_3; |.(f + g).| . x = |.((f + g) . x).| by A13, A18, MESFUNC1:def_10; then |.((|.(f + g).| |^ 2) . x).| = |.(|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|).| by A21, A22, Th9 .= |.|.(((f . x) + (g . x)) * ((f . x) + (g . x))).|.| by EXTREAL2:8 .= |.(((f . x) + (g . x)) * ((f . x) + (g . x))).| .= |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| by EXTREAL2:8 ; hence |.((|.(f + g).| |^ 2) . x).| < +infty by A20, XXREAL_0:9; ::_thesis: verum end; then |.(f + g).| |^ 2 is V67() by MESFUNC2:def_1; then A23: (1 / 4) (#) (|.(f + g).| |^ 2) is V67() by MESFUNC2:10; then A24: dom (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) = (dom ((1 / 4) (#) (|.(f + g).| |^ 2))) /\ (dom ((1 / 4) (#) (|.(f - g).| |^ 2))) by MESFUNC2:2; for x being Element of X st x in dom (f (#) g) holds (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x proof let x be Element of X; ::_thesis: ( x in dom (f (#) g) implies (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x ) assume A25: x in dom (f (#) g) ; ::_thesis: (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x then A26: |.(g . x).| < +infty by A3, A15, A16, A6, MESFUNC2:def_1; |.(f . x).| < +infty by A2, A15, A17, A6, A25, MESFUNC2:def_1; then reconsider c1 = f . x, c2 = g . x as Real by A26, EXTREAL2:30; (f . x) + (g . x) = c1 + c2 by SUPINF_2:1; then |.((f . x) + (g . x)).| = abs (c1 + c2) by EXTREAL2:1; then A27: |.((f . x) + (g . x)).| * |.((f . x) + (g . x)).| = (abs (c1 + c2)) * (abs (c1 + c2)) by EXTREAL1:1; ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| |^ 2) . x) by A15, A6, A7, A25, MESFUNC1:def_6; then ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f + g).| . x) |^ (1 + 1)) by A15, A6, A25, Def4; then A28: ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(f + g).| . x) |^ 1) * (|.(f + g).| . x)) by Th10; A29: |.(f + g).| . x = |.((f + g) . x).| by A13, A15, A6, A25, MESFUNC1:def_10; |.((f + g) . x).| = |.((f . x) + (g . x)).| by A14, A15, A6, A25, MESFUNC1:def_3; then ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) + (g . x)).| * |.((f . x) + (g . x)).|) by A29, A28, Th9; then A30: ((1 / 4) (#) (|.(f + g).| |^ 2)) . x = (1 / 4) * ((abs (c1 + c2)) * (abs (c1 + c2))) by A27, EXTREAL1:1; (abs (c1 - c2)) * (abs (c1 - c2)) = (abs (c1 - c2)) ^2 ; then A31: (abs (c1 - c2)) * (abs (c1 - c2)) = (c1 - c2) ^2 by COMPLEX1:75; ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| |^ 2) . x) by A10, A6, A12, A25, MESFUNC1:def_6; then ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * ((|.(f - g).| . x) |^ (1 + 1)) by A10, A6, A25, Def4; then A32: ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x)) by Th10; (f . x) - (g . x) = c1 - c2 by SUPINF_2:3; then |.((f . x) - (g . x)).| = abs (c1 - c2) by EXTREAL2:1; then A33: |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2)) by EXTREAL1:1; A34: |.(f - g).| . x = |.((f - g) . x).| by A8, A10, A6, A25, MESFUNC1:def_10; |.((f - g) . x).| = |.((f . x) - (g . x)).| by A9, A10, A6, A25, MESFUNC1:def_4; then ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (R_EAL (1 / 4)) * (|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|) by A34, A32, Th9; then A35: ((1 / 4) (#) (|.(f - g).| |^ 2)) . x = (1 / 4) * ((abs (c1 - c2)) * (abs (c1 - c2))) by A33, EXTREAL1:1; (abs (c1 + c2)) * (abs (c1 + c2)) = (abs (c1 + c2)) ^2 ; then (abs (c1 + c2)) * (abs (c1 + c2)) = (c1 + c2) ^2 by COMPLEX1:75; then (((1 / 4) (#) (|.(f + g).| |^ 2)) . x) - (((1 / 4) (#) (|.(f - g).| |^ 2)) . x) = ((1 / 4) * (((c1 ^2) + ((2 * c1) * c2)) + (c2 ^2))) - ((1 / 4) * (((c1 ^2) - ((2 * c1) * c2)) + (c2 ^2))) by A30, A35, A31, SUPINF_2:3 .= c1 * c2 .= (f . x) * (g . x) by EXTREAL1:1 .= (f (#) g) . x by A25, MESFUNC1:def_5 ; hence (f (#) g) . x = (((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2))) . x by A15, A10, A6, A7, A12, A24, A25, MESFUNC1:def_4; ::_thesis: verum end; then A36: f (#) g = ((1 / 4) (#) (|.(f + g).| |^ 2)) - ((1 / 4) (#) (|.(f - g).| |^ 2)) by A15, A10, A6, A7, A12, A24, PARTFUN1:5; A37: dom (|.(f - g).| |^ 2) c= dom f by A10, XBOOLE_1:17; for x being Element of X st x in dom (|.(f - g).| |^ 2) holds |.((|.(f - g).| |^ 2) . x).| < +infty proof let x be Element of X; ::_thesis: ( x in dom (|.(f - g).| |^ 2) implies |.((|.(f - g).| |^ 2) . x).| < +infty ) assume A38: x in dom (|.(f - g).| |^ 2) ; ::_thesis: |.((|.(f - g).| |^ 2) . x).| < +infty then A39: |.(g . x).| < +infty by A3, A11, MESFUNC2:def_1; |.(f . x).| < +infty by A2, A37, A38, MESFUNC2:def_1; then reconsider c1 = f . x, c2 = g . x as Real by A39, EXTREAL2:30; (f . x) - (g . x) = c1 - c2 by SUPINF_2:3; then |.((f . x) - (g . x)).| = abs (c1 - c2) by EXTREAL2:1; then A40: |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| = (abs (c1 - c2)) * (abs (c1 - c2)) by EXTREAL1:1; (|.(f - g).| |^ 2) . x = (|.(f - g).| . x) |^ (1 + 1) by A38, Def4; then A41: (|.(f - g).| |^ 2) . x = ((|.(f - g).| . x) |^ 1) * (|.(f - g).| . x) by Th10; |.(f - g).| . x = |.((f - g) . x).| by A8, A38, MESFUNC1:def_10; then |.(f - g).| . x = |.((f . x) - (g . x)).| by A9, A38, MESFUNC1:def_4; then |.((|.(f - g).| |^ 2) . x).| = |.(|.((f . x) - (g . x)).| * |.((f . x) - (g . x)).|).| by A41, Th9 .= |.|.(((f . x) - (g . x)) * ((f . x) - (g . x))).|.| by EXTREAL2:8 .= |.(((f . x) - (g . x)) * ((f . x) - (g . x))).| .= |.((f . x) - (g . x)).| * |.((f . x) - (g . x)).| by EXTREAL2:8 ; hence |.((|.(f - g).| |^ 2) . x).| < +infty by A40, XXREAL_0:9; ::_thesis: verum end; then |.(f - g).| |^ 2 is V67() by MESFUNC2:def_1; then A42: (1 / 4) (#) (|.(f - g).| |^ 2) is V67() by MESFUNC2:10; f + g is_measurable_on E by A2, A3, A4, A5, MESFUNC2:7; then |.(f + g).| |^ 2 is_measurable_on E by A1, A14, A15, Th14; then A43: (1 / 4) (#) (|.(f + g).| |^ 2) is_measurable_on E by A1, A15, MESFUNC5:49; f - g is_measurable_on E by A1, A2, A3, A4, A5, MESFUNC2:11, XBOOLE_1:17; then |.(f - g).| |^ 2 is_measurable_on E by A1, A9, A10, Th14; then (1 / 4) (#) (|.(f - g).| |^ 2) is_measurable_on E by A1, A10, MESFUNC5:49; hence f (#) g is_measurable_on E by A1, A10, A12, A23, A42, A36, A43, MESFUNC2:11; ::_thesis: verum end; theorem Th16: :: MESFUNC7:16 for X being non empty set for f being PartFunc of X,ExtREAL st rng f is real-bounded holds f is V67() proof let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL st rng f is real-bounded holds f is V67() let f be PartFunc of X,ExtREAL; ::_thesis: ( rng f is real-bounded implies f is V67() ) assume A1: rng f is real-bounded ; ::_thesis: f is V67() then rng f is bounded_above by XXREAL_2:def_11; then consider UB being real number such that A2: UB is UpperBound of rng f by XXREAL_2:def_10; A3: UB in REAL by XREAL_0:def_1; rng f is bounded_below by A1, XXREAL_2:def_11; then consider LB being real number such that A4: LB is LowerBound of rng f by XXREAL_2:def_9; A5: LB in REAL by XREAL_0:def_1; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_ |.(f_._x).|_<_+infty let x be Element of X; ::_thesis: ( x in dom f implies |.(f . x).| < +infty ) assume x in dom f ; ::_thesis: |.(f . x).| < +infty then A6: f . x in rng f by FUNCT_1:3; then LB <= f . x by A4, XXREAL_2:def_2; then -infty < f . x by A5, XXREAL_0:2, XXREAL_0:12; then A7: - +infty < f . x by XXREAL_3:23; f . x <= UB by A2, A6, XXREAL_2:def_1; then f . x < +infty by A3, XXREAL_0:2, XXREAL_0:9; hence |.(f . x).| < +infty by A7, EXTREAL2:11; ::_thesis: verum end; hence f is V67() by MESFUNC2:def_1; ::_thesis: verum end; theorem :: MESFUNC7:17 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL for E being Element of S for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL for E being Element of S for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL for E being Element of S for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL for E being Element of S for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) let E be Element of S; ::_thesis: for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M holds ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) let F be non empty Subset of ExtREAL; ::_thesis: ( (dom f) /\ (dom g) = E & rng f = F & g is V67() & f is_measurable_on E & rng f is real-bounded & g is_integrable_on M implies ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) ) assume that A1: (dom f) /\ (dom g) = E and A2: rng f = F and A3: g is V67() and A4: f is_measurable_on E and A5: rng f is real-bounded and A6: g is_integrable_on M ; ::_thesis: ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) A7: dom ((f (#) |.g.|) | E) = (dom (f (#) |.g.|)) /\ E by RELAT_1:61; A8: rng f is Subset of REAL by A5, Th16, MESFUNC2:32; then not +infty in rng f ; then A9: rng f <> {+infty} by TARSKI:def_1; A10: rng f is bounded_above by A5, XXREAL_2:def_11; not -infty in rng f by A8; then A11: rng f <> {-infty} by TARSKI:def_1; rng f is bounded_below by A5, XXREAL_2:def_11; then reconsider k0 = inf F, l0 = sup F as Real by A2, A10, A9, A11, XXREAL_2:57, XXREAL_2:58; A12: |.(sup F).| = abs l0 by EXTREAL2:1; |.(inf F).| = abs k0 by EXTREAL2:1; then reconsider k1 = |.(inf F).|, l1 = |.(sup F).| as Real by A12; A13: E c= dom f by A1, XBOOLE_1:17; A14: sup F is UpperBound of rng f by A2, XXREAL_2:def_3; A15: E c= dom g by A1, XBOOLE_1:17; then A16: E c= dom |.g.| by MESFUNC1:def_10; A17: dom |.g.| = dom g by MESFUNC1:def_10; for x being Element of X st x in dom |.g.| holds |.(|.g.| . x).| < +infty proof let x be Element of X; ::_thesis: ( x in dom |.g.| implies |.(|.g.| . x).| < +infty ) assume A18: x in dom |.g.| ; ::_thesis: |.(|.g.| . x).| < +infty then |.(|.g.| . x).| = |.|.(g . x).|.| by MESFUNC1:def_10; then |.(|.g.| . x).| = |.(g . x).| ; hence |.(|.g.| . x).| < +infty by A3, A17, A18, MESFUNC2:def_1; ::_thesis: verum end; then A19: |.g.| is V67() by MESFUNC2:def_1; A20: f is V67() by A5, Th16; consider E1 being Element of S such that A21: E1 = dom g and A22: g is_measurable_on E1 by A6, MESFUNC5:def_17; A23: E1 = dom |.g.| by A21, MESFUNC1:def_10; |.g.| is_measurable_on E1 by A21, A22, MESFUNC2:27; then A24: |.g.| is_measurable_on E by A1, A21, MESFUNC1:30, XBOOLE_1:17; (dom f) /\ (dom |.g.|) = E by A1, MESFUNC1:def_10; then A25: f (#) |.g.| is_measurable_on E by A4, A24, A20, A19, Th15; A26: |.g.| is_integrable_on M by A6, A21, A22, MESFUNC5:100; then A27: |.g.| | E is_integrable_on M by MESFUNC5:97; A28: dom (f (#) |.g.|) = (dom f) /\ (dom |.g.|) by MESFUNC1:def_5; then A29: dom (f (#) |.g.|) = E by A1, MESFUNC1:def_10; A30: dom (k0 (#) |.g.|) = dom |.g.| by MESFUNC1:def_6; then A31: dom ((k0 (#) |.g.|) | E) = E by A16, RELAT_1:62; A32: inf F is LowerBound of rng f by A2, XXREAL_2:def_4; A33: for x being Element of X st x in E holds ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) proof let x be Element of X; ::_thesis: ( x in E implies ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) ) A34: 0 <= |.(g . x).| by EXTREAL2:3; assume A35: x in E ; ::_thesis: ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) then A36: f . x <= sup F by A13, A14, FUNCT_1:3, XXREAL_2:def_1; inf F <= f . x by A13, A32, A35, FUNCT_1:3, XXREAL_2:def_2; hence ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) by A36, A34, XXREAL_3:71; ::_thesis: verum end; for x being Element of X st x in dom ((k0 (#) |.g.|) | E) holds ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x proof let x be Element of X; ::_thesis: ( x in dom ((k0 (#) |.g.|) | E) implies ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x ) assume A37: x in dom ((k0 (#) |.g.|) | E) ; ::_thesis: ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x then A38: ((k0 (#) |.g.|) | E) . x = (k0 (#) |.g.|) . x by FUNCT_1:47; (f (#) |.g.|) . x = (f . x) * (|.g.| . x) by A29, A31, A37, MESFUNC1:def_5; then A39: (f (#) |.g.|) . x = (f . x) * |.(g . x).| by A16, A31, A37, MESFUNC1:def_10; (k0 (#) |.g.|) . x = (R_EAL k0) * (|.g.| . x) by A16, A30, A31, A37, MESFUNC1:def_6; then (k0 (#) |.g.|) . x = (R_EAL k0) * |.(g . x).| by A16, A31, A37, MESFUNC1:def_10; then (k0 (#) |.g.|) . x <= (f (#) |.g.|) . x by A33, A31, A37, A39; hence ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x by A29, A7, A31, A37, A38, FUNCT_1:47; ::_thesis: verum end; then A40: ((f (#) |.g.|) | E) - ((k0 (#) |.g.|) | E) is nonnegative by Th1; A41: dom (l0 (#) |.g.|) = dom |.g.| by MESFUNC1:def_6; then A42: dom ((l0 (#) |.g.|) | E) = E by A16, RELAT_1:62; A43: dom (f (#) g) = E by A1, MESFUNC1:def_5; then A44: dom ((f (#) g) | E) = E by RELAT_1:62; then A45: dom |.((f (#) g) | E).| = E by MESFUNC1:def_10; A46: for x being Element of X st x in dom ((f (#) |.g.|) | E) holds |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x proof let x be Element of X; ::_thesis: ( x in dom ((f (#) |.g.|) | E) implies |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x ) assume A47: x in dom ((f (#) |.g.|) | E) ; ::_thesis: |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x then A48: ((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x by FUNCT_1:47; |.((f (#) |.g.|) . x).| = |.((f . x) * (|.g.| . x)).| by A29, A7, A47, MESFUNC1:def_5 .= |.((f . x) * |.(g . x).|).| by A1, A17, A15, A28, A7, A47, MESFUNC1:def_10 .= |.(f . x).| * |.|.(g . x).|.| by EXTREAL2:8 .= |.(f . x).| * |.(g . x).| ; then A49: |.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).| by EXTREAL2:8; dom |.(f (#) g).| = E by A43, MESFUNC1:def_10; then A50: |.(f (#) g).| . x = |.((f (#) g) . x).| by A29, A7, A47, MESFUNC1:def_10; |.(((f (#) g) | E) . x).| = |.((f (#) g) . x).| by A44, A29, A7, A47, FUNCT_1:47; then |.((f (#) g) | E).| . x = |.(f (#) g).| . x by A45, A29, A7, A47, A50, MESFUNC1:def_10; hence |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x by A43, A29, A7, A47, A49, A50, A48, MESFUNC1:def_5; ::_thesis: verum end; Integral (M,((l0 (#) |.g.|) | E)) = Integral (M,(l0 (#) (|.g.| | E))) by Th2; then A51: Integral (M,((l0 (#) |.g.|) | E)) = (R_EAL l0) * (Integral (M,(|.g.| | E))) by A27, MESFUNC5:110; A52: (dom (f (#) g)) /\ E = E by A43; g is_measurable_on E by A1, A21, A22, MESFUNC1:30, XBOOLE_1:17; then f (#) g is_measurable_on E by A1, A3, A4, A20, Th15; then A53: (f (#) g) | E is_measurable_on E by A52, MESFUNC5:42; A54: for x being Element of X st x in E holds |.(f . x).| <= |.(inf F).| + |.(sup F).| proof 0 <= abs k0 by COMPLEX1:46; then A55: l0 + 0 <= l0 + (abs k0) by XREAL_1:6; l0 <= abs l0 by COMPLEX1:76; then l0 + (abs k0) <= (abs l0) + (abs k0) by XREAL_1:6; then A56: l0 <= (abs l0) + (abs k0) by A55, XXREAL_0:2; 0 <= abs l0 by COMPLEX1:46; then A57: (- (abs k0)) - (abs l0) <= (- (abs k0)) - 0 by XREAL_1:10; - (abs k0) <= k0 by COMPLEX1:76; then A58: (- (abs k0)) - (abs l0) <= k0 by A57, XXREAL_0:2; let x be Element of X; ::_thesis: ( x in E implies |.(f . x).| <= |.(inf F).| + |.(sup F).| ) A59: abs k0 = |.(inf F).| by EXTREAL2:1; assume A60: x in E ; ::_thesis: |.(f . x).| <= |.(inf F).| + |.(sup F).| then f . x in rng f by A13, FUNCT_1:3; then reconsider fx = f . x as Real by A8; A61: abs l0 = |.(sup F).| by EXTREAL2:1; fx <= l0 by A13, A14, A60, FUNCT_1:3, XXREAL_2:def_1; then A62: fx <= (abs k0) + (abs l0) by A56, XXREAL_0:2; k0 <= fx by A13, A32, A60, FUNCT_1:3, XXREAL_2:def_2; then - ((abs k0) + (abs l0)) <= fx by A58, XXREAL_0:2; then A63: abs fx <= (abs k0) + (abs l0) by A62, ABSVALUE:5; abs fx = |.(f . x).| by EXTREAL2:1; hence |.(f . x).| <= |.(inf F).| + |.(sup F).| by A63, A59, A61, SUPINF_2:1; ::_thesis: verum end; dom (((k1 + l1) (#) |.g.|) | E) = dom ((k1 + l1) (#) (|.g.| | E)) by Th2; then dom (((k1 + l1) (#) |.g.|) | E) = dom (|.g.| | E) by MESFUNC1:def_6; then A64: dom (((k1 + l1) (#) |.g.|) | E) = E by A16, RELAT_1:62; A65: dom ((k1 + l1) (#) |.g.|) = dom |.g.| by MESFUNC1:def_6; A66: for x being Element of X st x in dom ((f (#) g) | E) holds |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x proof let x be Element of X; ::_thesis: ( x in dom ((f (#) g) | E) implies |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x ) assume A67: x in dom ((f (#) g) | E) ; ::_thesis: |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x then A68: ((f (#) g) | E) . x = (f (#) g) . x by FUNCT_1:47; dom (f | E) = E by A1, RELAT_1:62, XBOOLE_1:17; then A69: (f | E) . x = f . x by A44, A67, FUNCT_1:47; dom (g | E) = E by A1, RELAT_1:62, XBOOLE_1:17; then A70: (g | E) . x = g . x by A44, A67, FUNCT_1:47; 0 <= |.((g | E) . x).| by EXTREAL2:3; then A71: |.((f | E) . x).| * |.((g | E) . x).| <= (|.(inf F).| + |.(sup F).|) * |.((g | E) . x).| by A44, A54, A67, A69, XXREAL_3:71; A72: (((k1 + l1) (#) |.g.|) | E) . x = ((k1 + l1) (#) |.g.|) . x by A44, A64, A67, FUNCT_1:47; |.((f (#) g) . x).| = |.((f . x) * (g . x)).| by A43, A44, A67, MESFUNC1:def_5; then A73: |.(((f (#) g) | E) . x).| = |.((f | E) . x).| * |.((g | E) . x).| by A68, A69, A70, EXTREAL2:8; ((k1 + l1) (#) |.g.|) . x = (R_EAL (k1 + l1)) * (|.g.| . x) by A16, A44, A65, A67, MESFUNC1:def_6; then (((k1 + l1) (#) |.g.|) | E) . x = (R_EAL (k1 + l1)) * |.((g | E) . x).| by A16, A44, A67, A70, A72, MESFUNC1:def_10; hence |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x by A71, A73, SUPINF_2:1; ::_thesis: verum end; (k1 + l1) (#) |.g.| is_integrable_on M by A26, MESFUNC5:110; then A74: ((k1 + l1) (#) |.g.|) | E is_integrable_on M by MESFUNC5:97; then (f (#) g) | E is_integrable_on M by A44, A64, A53, A66, MESFUNC5:102; then A75: |.((f (#) g) | E).| is_integrable_on M by A44, A53, MESFUNC5:100; (dom (f (#) |.g.|)) /\ E = E by A29; then (f (#) |.g.|) | E is_measurable_on E by A25, MESFUNC5:42; then A76: (f (#) |.g.|) | E is_integrable_on M by A45, A29, A7, A75, A46, MESFUNC5:102; then A77: -infty < Integral (M,((f (#) |.g.|) | E)) by MESFUNC5:96; k0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:110; then (k0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:97; then consider V1 being Element of S such that A78: V1 = (dom ((k0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E)) and A79: Integral (M,(((k0 (#) |.g.|) | E) | V1)) <= Integral (M,(((f (#) |.g.|) | E) | V1)) by A76, A40, Th3; A80: ((f (#) |.g.|) | E) | V1 = (f (#) |.g.|) | E by A29, A7, A31, A78, RELAT_1:68; A81: dom (f (#) |.g.|) c= dom (l0 (#) |.g.|) by A28, A41, XBOOLE_1:17; for x being Element of X st x in dom ((f (#) |.g.|) | E) holds ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x proof let x be Element of X; ::_thesis: ( x in dom ((f (#) |.g.|) | E) implies ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x ) assume A82: x in dom ((f (#) |.g.|) | E) ; ::_thesis: ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x then A83: ((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x by FUNCT_1:47; (f (#) |.g.|) . x = (f . x) * (|.g.| . x) by A29, A7, A82, MESFUNC1:def_5; then A84: (f (#) |.g.|) . x = (f . x) * |.(g . x).| by A16, A29, A7, A82, MESFUNC1:def_10; (l0 (#) |.g.|) . x = (R_EAL l0) * (|.g.| . x) by A29, A7, A81, A82, MESFUNC1:def_6; then (l0 (#) |.g.|) . x = (R_EAL l0) * |.(g . x).| by A16, A29, A7, A82, MESFUNC1:def_10; then (f (#) |.g.|) . x <= (l0 (#) |.g.|) . x by A29, A7, A33, A82, A84; hence ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x by A29, A7, A42, A82, A83, FUNCT_1:47; ::_thesis: verum end; then A85: ((l0 (#) |.g.|) | E) - ((f (#) |.g.|) | E) is nonnegative by Th1; Integral (M,((k0 (#) |.g.|) | E)) = Integral (M,(k0 (#) (|.g.| | E))) by Th2; then A86: Integral (M,((k0 (#) |.g.|) | E)) = (R_EAL k0) * (Integral (M,(|.g.| | E))) by A27, MESFUNC5:110; l0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:110; then (l0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:97; then consider V2 being Element of S such that A87: V2 = (dom ((l0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E)) and A88: Integral (M,(((f (#) |.g.|) | E) | V2)) <= Integral (M,(((l0 (#) |.g.|) | E) | V2)) by A76, A85, Th3; A89: ((f (#) |.g.|) | E) | V2 = (f (#) |.g.|) | E by A29, A7, A42, A87, RELAT_1:68; A90: ((l0 (#) |.g.|) | E) | V2 = (l0 (#) |.g.|) | E by A29, A7, A42, A87, RELAT_1:68; A91: Integral (M,((f (#) |.g.|) | E)) < +infty by A76, MESFUNC5:96; A92: ((k0 (#) |.g.|) | E) | V1 = (k0 (#) |.g.|) | E by A29, A7, A31, A78, RELAT_1:68; ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) proof percases ( Integral (M,(|.g.| | E)) <> 0. or Integral (M,(|.g.| | E)) = 0. ) ; supposeA93: Integral (M,(|.g.| | E)) <> 0. ; ::_thesis: ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) reconsider c3 = Integral (M,((f (#) |.g.|) | E)) as Real by A77, A91, XXREAL_0:14; set c2 = (Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))); A94: Integral (M,(|.g.| | E)) < +infty by A27, MESFUNC5:96; A95: -infty < Integral (M,(|.g.| | E)) by A27, MESFUNC5:96; then reconsider c1 = Integral (M,(|.g.| | E)) as Real by A94, XXREAL_0:14; (Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) = c3 / c1 by EXTREAL1:2; then reconsider c = (Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) as Element of REAL ; A96: (Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))) = c1 / c1 by EXTREAL1:2; (Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))) = c1 / c1 by EXTREAL1:2; then A97: c3 * (c1 / c1) = (Integral (M,((f (#) |.g.|) | E))) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by EXTREAL1:1; (Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) = c3 / c1 by EXTREAL1:2; then (Integral (M,(|.g.| | E))) * ((Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E)))) = c1 * (c3 / c1) by EXTREAL1:1; then A98: (R_EAL c) * (Integral (M,(|.g.| | E))) = Integral (M,((f (#) |.g.|) | E)) by A93, A97, XXREAL_3:88; A99: Integral (M,(|.g.| | E)) > 0. by A21, A22, A23, A93, MESFUNC2:27, MESFUNC5:92; (sup F) * (Integral (M,(|.g.| | E))) = l0 * c1 by EXTREAL1:1; then A100: ((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (l0 * c1) / c1 by EXTREAL1:2; (l0 * c1) / c1 = l0 * (c1 / c1) ; then A101: ((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by A96, A100, EXTREAL1:1; (inf F) * (Integral (M,(|.g.| | E))) = k0 * c1 by EXTREAL1:1; then A102: ((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (k0 * c1) / c1 by EXTREAL1:2; (k0 * c1) / c1 = k0 * (c1 / c1) ; then A103: ((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) by A96, A102, EXTREAL1:1; (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = (sup F) * 1. by A93, A95, A94, XXREAL_3:78; then (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = sup F by XXREAL_3:81; then A104: c <= sup F by A51, A88, A89, A90, A99, A101, XXREAL_3:79; (inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = (inf F) * 1. by A93, A95, A94, XXREAL_3:78; then (inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = inf F by XXREAL_3:81; then c >= inf F by A86, A79, A92, A80, A99, A103, XXREAL_3:79; hence ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) by A104, A98; ::_thesis: verum end; supposeA105: Integral (M,(|.g.| | E)) = 0. ; ::_thesis: ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) then 0. <= Integral (M,((f (#) |.g.|) | E)) by A29, A7, A31, A86, A78, A79, A80, RELAT_1:68; then A106: Integral (M,((f (#) |.g.|) | E)) = 0. by A29, A7, A42, A51, A87, A88, A89, A105, RELAT_1:68; consider y being set such that A107: y in F by XBOOLE_0:def_1; reconsider y = y as Element of ExtREAL by A107; A108: y <= sup F by A107, XXREAL_2:4; inf F <= y by A107, XXREAL_2:3; then A109: k0 <= sup F by A108, XXREAL_0:2; (R_EAL k0) * (Integral (M,(|.g.| | E))) = 0. by A105; hence ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) by A109, A106; ::_thesis: verum end; end; end; hence ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st ( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = (R_EAL c) * (Integral (M,(|.g.| | E))) ) ) by A44, A64, A74, A53, A66, MESFUNC5:102; ::_thesis: verum end; begin theorem Th18: :: MESFUNC7:18 for X being non empty set for f being PartFunc of X,ExtREAL for A being set holds |.f.| | A = |.(f | A).| proof let X be non empty set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set holds |.f.| | A = |.(f | A).| let f be PartFunc of X,ExtREAL; ::_thesis: for A being set holds |.f.| | A = |.(f | A).| let A be set ; ::_thesis: |.f.| | A = |.(f | A).| dom (|.f.| | A) = (dom |.f.|) /\ A by RELAT_1:61; then A1: dom (|.f.| | A) = (dom f) /\ A by MESFUNC1:def_10; A2: dom (f | A) = (dom f) /\ A by RELAT_1:61; then A3: dom |.(f | A).| = (dom f) /\ A by MESFUNC1:def_10; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(|.f.|_|_A)_holds_ (|.f.|_|_A)_._x_=_|.(f_|_A).|_._x let x be Element of X; ::_thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x ) assume A4: x in dom (|.f.| | A) ; ::_thesis: (|.f.| | A) . x = |.(f | A).| . x then |.(f | A).| . x = |.((f | A) . x).| by A1, A3, MESFUNC1:def_10; then A5: |.(f | A).| . x = |.(f . x).| by A2, A1, A4, FUNCT_1:47; x in dom f by A1, A4, XBOOLE_0:def_4; then A6: x in dom |.f.| by MESFUNC1:def_10; (|.f.| | A) . x = |.f.| . x by A4, FUNCT_1:47; hence (|.f.| | A) . x = |.(f | A).| . x by A6, A5, MESFUNC1:def_10; ::_thesis: verum end; hence |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th19: :: MESFUNC7:19 for X being non empty set for f, g being PartFunc of X,ExtREAL holds ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL holds ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) set F = |.f.|; set G = |.g.|; |.f.| is V120() by MESFUNC5:12; then not -infty in rng |.f.| by MESFUNC5:def_3; then A1: |.f.| " {-infty} = {} by FUNCT_1:72; |.g.| is V120() by MESFUNC5:12; then not -infty in rng |.g.| by MESFUNC5:def_3; then A2: |.g.| " {-infty} = {} by FUNCT_1:72; dom (|.f.| + |.g.|) = ((dom |.f.|) /\ (dom |.g.|)) \ (((|.f.| " {-infty}) /\ (|.g.| " {+infty})) \/ ((|.f.| " {+infty}) /\ (|.g.| " {-infty}))) by MESFUNC1:def_3; then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by A1, A2, MESFUNC1:def_10; hence dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by MESFUNC1:def_10; ::_thesis: dom |.(f + g).| c= dom |.f.| dom |.(f + g).| = dom (f + g) by MESFUNC1:def_10 .= ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def_3 .= (dom f) /\ ((dom g) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))) by XBOOLE_1:49 ; then dom |.(f + g).| c= dom f by XBOOLE_1:17; hence dom |.(f + g).| c= dom |.f.| by MESFUNC1:def_10; ::_thesis: verum end; theorem Th20: :: MESFUNC7:20 for X being non empty set for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) let f, g be PartFunc of X,ExtREAL; ::_thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) A1: |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| by Th18; A2: dom |.(f + g).| c= dom |.g.| by Th19; then A3: dom |.(f + g).| c= dom g by MESFUNC1:def_10; dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61; then A4: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A3, XBOOLE_1:28; then A5: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by MESFUNC1:def_10; A6: dom |.(f + g).| c= dom |.f.| by Th19; then A7: dom |.(f + g).| c= dom f by MESFUNC1:def_10; then (dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A3, XBOOLE_1:27; then A8: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th19; then A9: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:62; dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) by RELAT_1:61; then A10: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A7, XBOOLE_1:28; A11: |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| by Th18; then A12: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by A1, Th19 .= dom |.(f + g).| by A10, A4 ; A13: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A10, MESFUNC1:def_10; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_holds_ ((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_._x_=_((|.f.|_|_(dom_|.(f_+_g).|))_+_(|.g.|_|_(dom_|.(f_+_g).|)))_._x let x be Element of X; ::_thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x ) assume A14: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; ::_thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x then A15: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47 .= (|.f.| . x) + (|.g.| . x) by A8, A9, A14, MESFUNC1:def_3 .= |.(f . x).| + (|.g.| . x) by A6, A9, A14, MESFUNC1:def_10 ; A16: x in dom |.(f + g).| by A8, A14, RELAT_1:62; then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A12, MESFUNC1:def_3 .= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A13, A11, A1, A16, MESFUNC1:def_10 .= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A5, A16, MESFUNC1:def_10 .= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A16, FUNCT_1:49 .= |.(f . x).| + |.(g . x).| by A16, FUNCT_1:49 ; hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A2, A9, A14, A15, MESFUNC1:def_10; ::_thesis: verum end; hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A12, A8, PARTFUN1:5, RELAT_1:62; ::_thesis: verum end; theorem Th21: :: MESFUNC7:21 for X being non empty set for f, g being PartFunc of X,ExtREAL for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,ExtREAL for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x let f, g be PartFunc of X,ExtREAL; ::_thesis: for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x let x be set ; ::_thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x ) A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL2:13; assume A2: x in dom |.(f + g).| ; ::_thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x then x in dom (f + g) by MESFUNC1:def_10; then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, MESFUNC1:def_3; A4: dom |.(f + g).| c= dom |.g.| by Th19; then A5: |.(g . x).| = |.g.| . x by A2, MESFUNC1:def_10; x in dom |.g.| by A2, A4; then A6: x in dom g by MESFUNC1:def_10; A7: dom |.(f + g).| c= dom |.f.| by Th19; then x in dom |.f.| by A2; then x in dom f by MESFUNC1:def_10; then x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4; then A8: x in dom (|.f.| + |.g.|) by Th19; |.(f . x).| = |.f.| . x by A2, A7, MESFUNC1:def_10; then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, MESFUNC1:def_3; hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, MESFUNC1:def_10; ::_thesis: verum end; theorem :: MESFUNC7:22 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) ex A being Element of S st ( A = dom g & g is_measurable_on A ) by A2, MESFUNC5:def_17; then A3: |.g.| is_integrable_on M by A2, MESFUNC5:100; A4: f + g is_integrable_on M by A1, A2, MESFUNC5:108; then ex A being Element of S st ( A = dom (f + g) & f + g is_measurable_on A ) by MESFUNC5:def_17; then A5: |.(f + g).| is_integrable_on M by A4, MESFUNC5:100; for x being Element of X st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x by Th21; then A6: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th1; set G = |.g.|; set F = |.f.|; A7: dom |.(f + g).| = dom (f + g) by MESFUNC1:def_10 .= ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def_3 ; ex A being Element of S st ( A = dom f & f is_measurable_on A ) by A1, MESFUNC5:def_17; then A8: |.f.| is_integrable_on M by A1, MESFUNC5:100; then |.f.| + |.g.| is_integrable_on M by A3, MESFUNC5:108; then consider E being Element of S such that A9: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and A10: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A5, A6, Th3; A11: |.g.| | E is_integrable_on M by A3, MESFUNC5:97; |.f.| | E is_integrable_on M by A8, MESFUNC5:97; then consider E1 being Element of S such that A12: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and A13: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by A11, MESFUNC5:109; take E ; ::_thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) dom (|.g.| | E) = (dom |.g.|) /\ E by RELAT_1:61; then A14: dom (|.g.| | E) = (dom g) /\ E by MESFUNC1:def_10; A15: dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by Th19; then A16: E = dom |.(f + g).| by A9, A7, XBOOLE_1:28, XBOOLE_1:36; dom (|.f.| | E) = (dom |.f.|) /\ E by RELAT_1:61; then dom (|.f.| | E) = (dom f) /\ E by MESFUNC1:def_10; then E1 = (((dom f) /\ E) /\ E) /\ (dom g) by A12, A14, XBOOLE_1:16; then E1 = ((dom f) /\ (E /\ E)) /\ (dom g) by XBOOLE_1:16; then E1 = ((dom f) /\ (dom g)) /\ E by XBOOLE_1:16; then A17: E1 = E by A9, A15, A7, XBOOLE_1:28, XBOOLE_1:36; then A18: (|.g.| | E) | E1 = |.g.| | E by FUNCT_1:51; (|.f.| | E) | E1 = |.f.| | E by A17, FUNCT_1:51; hence ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) by A10, A13, A16, A18, Th20, MESFUNC1:def_10; ::_thesis: verum end; theorem Th23: :: MESFUNC7:23 for X being non empty set for A being set holds max+ (chi (A,X)) = chi (A,X) proof let X be non empty set ; ::_thesis: for A being set holds max+ (chi (A,X)) = chi (A,X) let A be set ; ::_thesis: max+ (chi (A,X)) = chi (A,X) A1: dom (max+ (chi (A,X))) = dom (chi (A,X)) by MESFUNC2:def_2; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(max+_(chi_(A,X)))_holds_ (max+_(chi_(A,X)))_._x_=_(chi_(A,X))_._x let x be Element of X; ::_thesis: ( x in dom (max+ (chi (A,X))) implies (max+ (chi (A,X))) . x = (chi (A,X)) . x ) A2: rng (chi (A,X)) c= {0,1} by FUNCT_3:39; assume A3: x in dom (max+ (chi (A,X))) ; ::_thesis: (max+ (chi (A,X))) . x = (chi (A,X)) . x then A4: (max+ (chi (A,X))) . x = max (((chi (A,X)) . x),0.) by MESFUNC2:def_2; (chi (A,X)) . x in rng (chi (A,X)) by A1, A3, FUNCT_1:3; hence (max+ (chi (A,X))) . x = (chi (A,X)) . x by A4, A2, XXREAL_0:def_10; ::_thesis: verum end; hence max+ (chi (A,X)) = chi (A,X) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th24: :: MESFUNC7:24 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st M . E < +infty holds ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st M . E < +infty holds ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S st M . E < +infty holds ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) let M be sigma_Measure of S; ::_thesis: for E being Element of S st M . E < +infty holds ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) let E be Element of S; ::_thesis: ( M . E < +infty implies ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) ) reconsider XX = X as Element of S by MEASURE1:7; set F = XX \ E; A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(max-_(chi_(E,X)))_holds_ (max-_(chi_(E,X)))_._x_=_0 let x be Element of X; ::_thesis: ( x in dom (max- (chi (E,X))) implies (max- (chi (E,X))) . x = 0 ) A2: now__::_thesis:_(_x_in_E_implies_max_((-_((chi_(E,X))_._x)),0.)_=_0._) assume x in E ; ::_thesis: max ((- ((chi (E,X)) . x)),0.) = 0. then (chi (E,X)) . x = 1 by FUNCT_3:def_3; hence max ((- ((chi (E,X)) . x)),0.) = 0. by XXREAL_0:def_10; ::_thesis: verum end; A3: now__::_thesis:_(_not_x_in_E_implies_max_((-_((chi_(E,X))_._x)),0.)_=_0._) assume not x in E ; ::_thesis: max ((- ((chi (E,X)) . x)),0.) = 0. then (chi (E,X)) . x = 0. by FUNCT_3:def_3; then - ((chi (E,X)) . x) = 0 ; hence max ((- ((chi (E,X)) . x)),0.) = 0. ; ::_thesis: verum end; assume x in dom (max- (chi (E,X))) ; ::_thesis: (max- (chi (E,X))) . x = 0 hence (max- (chi (E,X))) . x = 0 by A2, A3, MESFUNC2:def_3; ::_thesis: verum end; A4: XX = dom (chi (E,X)) by FUNCT_3:def_3; then A5: XX = dom (max+ (chi (E,X))) by Th23; A6: XX /\ (XX \ E) = XX \ E by XBOOLE_1:28; then A7: dom ((max+ (chi (E,X))) | (XX \ E)) = XX \ E by A5, RELAT_1:61; A8: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((max+_(chi_(E,X)))_|_(XX_\_E))_holds_ ((max+_(chi_(E,X)))_|_(XX_\_E))_._x_=_0 let x be Element of X; ::_thesis: ( x in dom ((max+ (chi (E,X))) | (XX \ E)) implies ((max+ (chi (E,X))) | (XX \ E)) . x = 0 ) assume A9: x in dom ((max+ (chi (E,X))) | (XX \ E)) ; ::_thesis: ((max+ (chi (E,X))) | (XX \ E)) . x = 0 then (chi (E,X)) . x = 0 by A7, FUNCT_3:37; then (max+ (chi (E,X))) . x = 0 by Th23; hence ((max+ (chi (E,X))) | (XX \ E)) . x = 0 by A9, FUNCT_1:47; ::_thesis: verum end; A10: chi (E,X) is_measurable_on XX by MESFUNC2:29; then A11: max+ (chi (E,X)) is_measurable_on XX by Th23; then max+ (chi (E,X)) is_measurable_on XX \ E by MESFUNC1:30; then A12: integral+ (M,((max+ (chi (E,X))) | (XX \ E))) = 0 by A5, A6, A7, A8, MESFUNC5:42, MESFUNC5:87; XX = dom (max- (chi (E,X))) by A4, MESFUNC2:def_3; then A13: integral+ (M,(max- (chi (E,X)))) = 0 by A4, A10, A1, MESFUNC2:26, MESFUNC5:87; A14: XX /\ E = E by XBOOLE_1:28; then A15: dom ((max+ (chi (E,X))) | E) = E by A5, RELAT_1:61; E \/ (XX \ E) = XX by A14, XBOOLE_1:51; then A16: (max+ (chi (E,X))) | (E \/ (XX \ E)) = max+ (chi (E,X)) by A5, RELAT_1:69; A17: for x being set st x in dom (max+ (chi (E,X))) holds 0. <= (max+ (chi (E,X))) . x by MESFUNC2:12; then A18: max+ (chi (E,X)) is nonnegative by SUPINF_2:52; then integral+ (M,((max+ (chi (E,X))) | (E \/ (XX \ E)))) = (integral+ (M,((max+ (chi (E,X))) | E))) + (integral+ (M,((max+ (chi (E,X))) | (XX \ E)))) by A5, A11, MESFUNC5:81, XBOOLE_1:79; then A19: integral+ (M,(max+ (chi (E,X)))) = integral+ (M,((max+ (chi (E,X))) | E)) by A16, A12, XXREAL_3:4; A20: now__::_thesis:_for_x_being_set_st_x_in_dom_((max+_(chi_(E,X)))_|_E)_holds_ ((max+_(chi_(E,X)))_|_E)_._x_=_1 let x be set ; ::_thesis: ( x in dom ((max+ (chi (E,X))) | E) implies ((max+ (chi (E,X))) | E) . x = 1 ) assume A21: x in dom ((max+ (chi (E,X))) | E) ; ::_thesis: ((max+ (chi (E,X))) | E) . x = 1 then (chi (E,X)) . x = 1 by A15, FUNCT_3:def_3; then (max+ (chi (E,X))) . x = 1 by Th23; hence ((max+ (chi (E,X))) | E) . x = 1 by A21, FUNCT_1:47; ::_thesis: verum end; then (max+ (chi (E,X))) | E is_simple_func_in S by A15, MESFUNC6:2; then integral+ (M,(max+ (chi (E,X)))) = integral' (M,((max+ (chi (E,X))) | E)) by A18, A19, MESFUNC5:15, MESFUNC5:77; then A22: integral+ (M,(max+ (chi (E,X)))) = (R_EAL 1) * (M . (dom ((max+ (chi (E,X))) | E))) by A15, A20, MESFUNC5:104; max+ (chi (E,X)) is_measurable_on E by A11, MESFUNC1:30; then (max+ (chi (E,X))) | E is_measurable_on E by A5, A14, MESFUNC5:42; then A23: (chi (E,X)) | E is_measurable_on E by Th23; (max+ (chi (E,X))) | E is nonnegative by A17, MESFUNC5:15, SUPINF_2:52; then A24: (chi (E,X)) | E is nonnegative by Th23; E = dom ((chi (E,X)) | E) by A15, Th23; then A25: Integral (M,((chi (E,X)) | E)) = integral+ (M,((chi (E,X)) | E)) by A23, A24, MESFUNC5:88; assume M . E < +infty ; ::_thesis: ( chi (E,X) is_integrable_on M & Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) then integral+ (M,(max+ (chi (E,X)))) < +infty by A15, A22, XXREAL_3:81; hence chi (E,X) is_integrable_on M by A4, A10, A13, MESFUNC5:def_17; ::_thesis: ( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E ) Integral (M,(chi (E,X))) = (R_EAL 1) * (M . E) by A15, A22, A13, XXREAL_3:15; hence Integral (M,(chi (E,X))) = M . E by XXREAL_3:81; ::_thesis: Integral (M,((chi (E,X)) | E)) = M . E (chi (E,X)) | E = (max+ (chi (E,X))) | E by Th23; hence Integral (M,((chi (E,X)) | E)) = M . E by A15, A19, A22, A25, XXREAL_3:81; ::_thesis: verum end; theorem Th25: :: MESFUNC7:25 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) let M be sigma_Measure of S; ::_thesis: for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) let E1, E2 be Element of S; ::_thesis: ( M . (E1 /\ E2) < +infty implies Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) ) reconsider XX = X as Element of S by MEASURE1:7; A1: E2 = (E1 /\ E2) \/ (E2 \ E1) by XBOOLE_1:51; set F = E2 \ E1; A2: dom ((chi (E1,X)) | (E1 /\ E2)) = (dom (chi (E1,X))) /\ (E1 /\ E2) by RELAT_1:61 .= X /\ (E1 /\ E2) by FUNCT_3:def_3 ; A3: dom ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) = (dom (chi ((E1 /\ E2),X))) /\ (E1 /\ E2) by RELAT_1:61 .= X /\ (E1 /\ E2) by FUNCT_3:def_3 ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((chi_(E1,X))_|_(E1_/\_E2))_holds_ ((chi_(E1,X))_|_(E1_/\_E2))_._x_=_((chi_((E1_/\_E2),X))_|_(E1_/\_E2))_._x let x be Element of X; ::_thesis: ( x in dom ((chi (E1,X)) | (E1 /\ E2)) implies ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x ) assume A4: x in dom ((chi (E1,X)) | (E1 /\ E2)) ; ::_thesis: ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x then A5: ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x = (chi ((E1 /\ E2),X)) . x by A2, A3, FUNCT_1:47; A6: x in E1 /\ E2 by A2, A4, XBOOLE_0:def_4; then A7: x in E1 by XBOOLE_0:def_4; ((chi (E1,X)) | (E1 /\ E2)) . x = (chi (E1,X)) . x by A4, FUNCT_1:47 .= 1 by A7, FUNCT_3:def_3 ; hence ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x by A6, A5, FUNCT_3:def_3; ::_thesis: verum end; then A8: (chi (E1,X)) | (E1 /\ E2) = (chi ((E1 /\ E2),X)) | (E1 /\ E2) by A2, A3, PARTFUN1:5; assume M . (E1 /\ E2) < +infty ; ::_thesis: Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) then A9: Integral (M,((chi (E1,X)) | (E1 /\ E2))) = M . (E1 /\ E2) by A8, Th24; A10: XX = dom (chi (E1,X)) by FUNCT_3:def_3; then A11: E2 \ E1 = dom ((chi (E1,X)) | (E2 \ E1)) by RELAT_1:62; then E2 \ E1 = (dom (chi (E1,X))) /\ (E2 \ E1) by RELAT_1:61; then A12: (chi (E1,X)) | (E2 \ E1) is_measurable_on E2 \ E1 by MESFUNC2:29, MESFUNC5:42; now__::_thesis:_for_x_being_set_st_x_in_dom_(chi_(E1,X))_holds_ 0._<=_(chi_(E1,X))_._x let x be set ; ::_thesis: ( x in dom (chi (E1,X)) implies 0. <= (chi (E1,X)) . x ) assume x in dom (chi (E1,X)) ; ::_thesis: 0. <= (chi (E1,X)) . x then A13: (chi (E1,X)) . x in rng (chi (E1,X)) by FUNCT_1:3; rng (chi (E1,X)) c= {0,1} by FUNCT_3:39; hence 0. <= (chi (E1,X)) . x by A13; ::_thesis: verum end; then A14: chi (E1,X) is nonnegative by SUPINF_2:52; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((chi_(E1,X))_|_(E2_\_E1))_holds_ 0_=_((chi_(E1,X))_|_(E2_\_E1))_._x let x be Element of X; ::_thesis: ( x in dom ((chi (E1,X)) | (E2 \ E1)) implies 0 = ((chi (E1,X)) | (E2 \ E1)) . x ) assume A15: x in dom ((chi (E1,X)) | (E2 \ E1)) ; ::_thesis: 0 = ((chi (E1,X)) | (E2 \ E1)) . x E2 \ E1 c= X \ E1 by XBOOLE_1:33; then (chi (E1,X)) . x = 0 by A11, A15, FUNCT_3:37; hence 0 = ((chi (E1,X)) | (E2 \ E1)) . x by A15, FUNCT_1:47; ::_thesis: verum end; then integral+ (M,((chi (E1,X)) | (E2 \ E1))) = 0 by A11, A12, MESFUNC5:87; then A16: Integral (M,((chi (E1,X)) | (E2 \ E1))) = 0. by A14, A11, A12, MESFUNC5:15, MESFUNC5:88; chi (E1,X) is_measurable_on XX by MESFUNC2:29; then Integral (M,((chi (E1,X)) | E2)) = (Integral (M,((chi (E1,X)) | (E1 /\ E2)))) + (Integral (M,((chi (E1,X)) | (E2 \ E1)))) by A10, A14, A1, MESFUNC5:91, XBOOLE_1:89; hence Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) by A9, A16, XXREAL_3:4; ::_thesis: verum end; theorem :: MESFUNC7:26 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for E being Element of S for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL for E being Element of S for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) let f be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) let E be Element of S; ::_thesis: for a, b being real number st f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) holds ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) let a, b be real number ; ::_thesis: ( f is_integrable_on M & E c= dom f & M . E < +infty & ( for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ) implies ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) ) reconsider a1 = a, b1 = b as Element of REAL by XREAL_0:def_1; assume that A1: f is_integrable_on M and A2: E c= dom f and A3: M . E < +infty and A4: for x being Element of X st x in E holds ( a <= f . x & f . x <= b ) ; ::_thesis: ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) set C = chi (E,X); A5: f | E is_integrable_on M by A1, MESFUNC5:97; for x being Element of X st x in dom (a1 (#) ((chi (E,X)) | E)) holds (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x proof let x be Element of X; ::_thesis: ( x in dom (a1 (#) ((chi (E,X)) | E)) implies (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x ) assume A6: x in dom (a1 (#) ((chi (E,X)) | E)) ; ::_thesis: (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x then A7: x in dom ((chi (E,X)) | E) by MESFUNC1:def_6; then x in (dom (chi (E,X))) /\ E by RELAT_1:61; then A8: x in E by XBOOLE_0:def_4; then a <= f . x by A4; then A9: a <= (f | E) . x by A8, FUNCT_1:49; (a1 (#) ((chi (E,X)) | E)) . x = (R_EAL a) * (((chi (E,X)) | E) . x) by A6, MESFUNC1:def_6 .= (R_EAL a) * ((chi (E,X)) . x) by A7, FUNCT_1:47 .= (R_EAL a) * 1. by A8, FUNCT_3:def_3 ; hence (a1 (#) ((chi (E,X)) | E)) . x <= (f | E) . x by A9, XXREAL_3:81; ::_thesis: verum end; then A10: (f | E) - (a1 (#) ((chi (E,X)) | E)) is nonnegative by Th1; chi (E,X) is_integrable_on M by A3, Th24; then A11: (chi (E,X)) | E is_integrable_on M by MESFUNC5:97; then a1 (#) ((chi (E,X)) | E) is_integrable_on M by MESFUNC5:110; then consider E1 being Element of S such that A12: E1 = (dom (f | E)) /\ (dom (a1 (#) ((chi (E,X)) | E))) and A13: Integral (M,((a1 (#) ((chi (E,X)) | E)) | E1)) <= Integral (M,((f | E) | E1)) by A5, A10, Th3; dom (f | E) = (dom f) /\ E by RELAT_1:61; then A14: dom (f | E) = E by A2, XBOOLE_1:28; dom (a1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6; then dom (a1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61; then dom (a1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3; then A15: dom (a1 (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28; then A16: (f | E) | E1 = f | E by A12, A14, RELAT_1:69; dom (b1 (#) ((chi (E,X)) | E)) = dom ((chi (E,X)) | E) by MESFUNC1:def_6; then dom (b1 (#) ((chi (E,X)) | E)) = (dom (chi (E,X))) /\ E by RELAT_1:61; then dom (b1 (#) ((chi (E,X)) | E)) = X /\ E by FUNCT_3:def_3; then A17: dom (b1 (#) ((chi (E,X)) | E)) = E by XBOOLE_1:28; for x being Element of X st x in dom (f | E) holds (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x proof let x be Element of X; ::_thesis: ( x in dom (f | E) implies (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x ) assume A18: x in dom (f | E) ; ::_thesis: (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x then A19: x in dom ((chi (E,X)) | E) by A14, A15, MESFUNC1:def_6; then x in (dom (chi (E,X))) /\ E by RELAT_1:61; then A20: x in E by XBOOLE_0:def_4; then f . x <= b by A4; then A21: (f | E) . x <= b by A20, FUNCT_1:49; (b1 (#) ((chi (E,X)) | E)) . x = (R_EAL b) * (((chi (E,X)) | E) . x) by A14, A17, A18, MESFUNC1:def_6 .= (R_EAL b) * ((chi (E,X)) . x) by A19, FUNCT_1:47 .= (R_EAL b) * 1. by A20, FUNCT_3:def_3 ; hence (f | E) . x <= (b1 (#) ((chi (E,X)) | E)) . x by A21, XXREAL_3:81; ::_thesis: verum end; then A22: (b1 (#) ((chi (E,X)) | E)) - (f | E) is nonnegative by Th1; b1 (#) ((chi (E,X)) | E) is_integrable_on M by A11, MESFUNC5:110; then consider E2 being Element of S such that A23: E2 = (dom (f | E)) /\ (dom (b1 (#) ((chi (E,X)) | E))) and A24: Integral (M,((f | E) | E2)) <= Integral (M,((b1 (#) ((chi (E,X)) | E)) | E2)) by A5, A22, Th3; A25: (b1 (#) ((chi (E,X)) | E)) | E2 = b1 (#) ((chi (E,X)) | E) by A14, A17, A23, RELAT_1:69; E = E /\ E ; then A26: Integral (M,((chi (E,X)) | E)) = M . E by A3, Th25; A27: (f | E) | E2 = f | E by A14, A17, A23, RELAT_1:69; (a1 (#) ((chi (E,X)) | E)) | E1 = a1 (#) ((chi (E,X)) | E) by A12, A14, A15, RELAT_1:69; hence ( (R_EAL a) * (M . E) <= Integral (M,(f | E)) & Integral (M,(f | E)) <= (R_EAL b) * (M . E) ) by A11, A13, A24, A25, A16, A27, A26, MESFUNC5:110; ::_thesis: verum end;