:: MESFUNC6 semantic presentation begin theorem Th1: :: MESFUNC6:1 for X being non empty set for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f) let f be PartFunc of X,REAL; ::_thesis: |.(R_EAL f).| = R_EAL (abs f) A1: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_|.(R_EAL_f).|_holds_ |.(R_EAL_f).|_._x_=_(R_EAL_(abs_f))_._x let x be Element of X; ::_thesis: ( x in dom |.(R_EAL f).| implies |.(R_EAL f).| . x = (R_EAL (abs f)) . x ) assume x in dom |.(R_EAL f).| ; ::_thesis: |.(R_EAL f).| . x = (R_EAL (abs f)) . x then |.(R_EAL f).| . x = |.((R_EAL f) . x).| by MESFUNC1:def_10; then |.(R_EAL f).| . x = abs (f . x) by EXTREAL2:1; hence |.(R_EAL f).| . x = (R_EAL (abs f)) . x by VALUED_1:18; ::_thesis: verum end; dom |.(R_EAL f).| = dom (R_EAL f) by MESFUNC1:def_10 .= dom (abs f) by VALUED_1:def_11 ; hence |.(R_EAL f).| = R_EAL (abs f) by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th2: :: MESFUNC6:2 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 r being Real st dom f in S & ( for x being set st x in dom f holds f . x = r ) holds f is_simple_func_in S 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 r being Real st dom f in S & ( for x being set st x in dom f holds f . x = r ) holds f is_simple_func_in S let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL for r being Real st dom f in S & ( for x being set st x in dom f holds f . x = r ) holds f is_simple_func_in S let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL for r being Real st dom f in S & ( for x being set st x in dom f holds f . x = r ) holds f is_simple_func_in S let f be PartFunc of X,ExtREAL; ::_thesis: for r being Real st dom f in S & ( for x being set st x in dom f holds f . x = r ) holds f is_simple_func_in S let r be Real; ::_thesis: ( dom f in S & ( for x being set st x in dom f holds f . x = r ) implies f is_simple_func_in S ) assume that A1: dom f in S and A2: for x being set st x in dom f holds f . x = r ; ::_thesis: f is_simple_func_in S reconsider Df = dom f as Element of S by A1; A3: ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) proof set F = <*Df*>; A4: dom <*Df*> = Seg 1 by FINSEQ_1:38; A5: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_<*Df*>_&_j_in_dom_<*Df*>_&_i_<>_j_holds_ <*Df*>_._i_misses_<*Df*>_._j let i, j be Nat; ::_thesis: ( i in dom <*Df*> & j in dom <*Df*> & i <> j implies <*Df*> . i misses <*Df*> . j ) assume that A6: i in dom <*Df*> and A7: ( j in dom <*Df*> & i <> j ) ; ::_thesis: <*Df*> . i misses <*Df*> . j i = 1 by A4, A6, FINSEQ_1:2, TARSKI:def_1; hence <*Df*> . i misses <*Df*> . j by A4, A7, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; A8: for n being Nat st n in dom <*Df*> holds <*Df*> . n = Df proof let n be Nat; ::_thesis: ( n in dom <*Df*> implies <*Df*> . n = Df ) assume n in dom <*Df*> ; ::_thesis: <*Df*> . n = Df then n = 1 by A4, FINSEQ_1:2, TARSKI:def_1; hence <*Df*> . n = Df by FINSEQ_1:40; ::_thesis: verum end; reconsider F = <*Df*> as Finite_Sep_Sequence of S by A5, MESFUNC3:4; take F ; ::_thesis: ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) F = <*(F . 1)*> by FINSEQ_1:40; then A9: rng F = {(F . 1)} by FINSEQ_1:38; 1 in Seg 1 ; then F . 1 = Df by A4, A8; hence dom f = union (rng F) by A9, ZFMISC_1:25; ::_thesis: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y hereby ::_thesis: verum let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y ) assume that A10: n in dom F and A11: x in F . n and A12: y in F . n ; ::_thesis: f . x = f . y A13: F . n = Df by A8, A10; then f . x = r by A2, A11; hence f . x = f . y by A2, A12, A13; ::_thesis: verum end; end; 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 A14: f . x = r by A2; then -infty < f . x by XXREAL_0:12; then A15: - +infty < f . x by XXREAL_3:def_3; f . x < +infty by A14, XXREAL_0:9; hence |.(f . x).| < +infty by A15, EXTREAL2:11; ::_thesis: verum end; then f is V68() by MESFUNC2:def_1; hence f is_simple_func_in S by A3, MESFUNC2:def_4; ::_thesis: verum end; theorem :: MESFUNC6:3 for X being non empty set for f being PartFunc of X,REAL for a being real number for x being set holds ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for a being real number for x being set holds ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) let f be PartFunc of X,REAL; ::_thesis: for a being real number for x being set holds ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) let a be real number ; ::_thesis: for x being set holds ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) let x be set ; ::_thesis: ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) ( ex y being Real st ( y = f . x & y < a ) iff f . x < R_EAL a ) ; hence ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y < a ) ) ) by MESFUNC1:def_11; ::_thesis: verum end; theorem :: MESFUNC6:4 for X being non empty set for f being PartFunc of X,REAL for a being real number for x being set holds ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for a being real number for x being set holds ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) let f be PartFunc of X,REAL; ::_thesis: for a being real number for x being set holds ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) let a be real number ; ::_thesis: for x being set holds ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) let x be set ; ::_thesis: ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) ( ex y being Real st ( y = f . x & y <= a ) iff f . x <= R_EAL a ) ; hence ( x in less_eq_dom (f,a) iff ( x in dom f & ex y being Real st ( y = f . x & y <= a ) ) ) by MESFUNC1:def_12; ::_thesis: verum end; theorem :: MESFUNC6:5 for X being non empty set for f being PartFunc of X,REAL for r being Real for x being set holds ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real for x being set holds ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real for x being set holds ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) let r be Real; ::_thesis: for x being set holds ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) let x be set ; ::_thesis: ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) ( ex y being Real st ( y = f . x & r < y ) iff R_EAL r < f . x ) ; hence ( x in great_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r < y ) ) ) by MESFUNC1:def_13; ::_thesis: verum end; theorem :: MESFUNC6:6 for X being non empty set for f being PartFunc of X,REAL for r being Real for x being set holds ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real for x being set holds ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real for x being set holds ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) let r be Real; ::_thesis: for x being set holds ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) let x be set ; ::_thesis: ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) ( ex y being Real st ( y = f . x & r <= y ) iff R_EAL r <= f . x ) ; hence ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r <= y ) ) ) by MESFUNC1:def_14; ::_thesis: verum end; theorem :: MESFUNC6:7 for X being non empty set for f being PartFunc of X,REAL for r being Real for x being set holds ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real for x being set holds ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real for x being set holds ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) let r be Real; ::_thesis: for x being set holds ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) let x be set ; ::_thesis: ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) ( ex y being Real st ( y = f . x & r = y ) iff R_EAL r = f . x ) ; hence ( x in eq_dom (f,r) iff ( x in dom f & ex y being Real st ( y = f . x & r = y ) ) ) by MESFUNC1:def_15; ::_thesis: verum end; theorem :: MESFUNC6:8 for X being non empty set for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) proof let X be non empty set ; ::_thesis: for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) let Y be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (great_eq_dom (f,r)) = meet (rng F) let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) implies Y /\ (great_eq_dom (f,r)) = meet (rng F) ) assume for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ; ::_thesis: Y /\ (great_eq_dom (f,r)) = meet (rng F) then for n being Element of NAT holds F . n = Y /\ (great_dom ((R_EAL f),(R_EAL (r - (1 / (n + 1)))))) ; then Y /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) by MESFUNC1:19; hence Y /\ (great_eq_dom (f,r)) = meet (rng F) ; ::_thesis: verum end; theorem :: MESFUNC6:9 for X being non empty set for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) proof let X be non empty set ; ::_thesis: for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) let Y be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (less_eq_dom (f,r)) = meet (rng F) let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (less_eq_dom (f,r)) = meet (rng F) ) assume for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ; ::_thesis: Y /\ (less_eq_dom (f,r)) = meet (rng F) then for n being Element of NAT holds F . n = Y /\ (less_dom ((R_EAL f),(R_EAL (r + (1 / (n + 1)))))) ; then Y /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) by MESFUNC1:20; hence Y /\ (less_eq_dom (f,r)) = meet (rng F) ; ::_thesis: verum end; theorem :: MESFUNC6:10 for X being non empty set for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) proof let X be non empty set ; ::_thesis: for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) let Y be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds Y /\ (less_dom (f,r)) = union (rng F) let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) implies Y /\ (less_dom (f,r)) = union (rng F) ) assume for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ; ::_thesis: Y /\ (less_dom (f,r)) = union (rng F) then for n being Element of NAT holds F . n = Y /\ (less_eq_dom ((R_EAL f),(R_EAL (r - (1 / (n + 1)))))) ; then Y /\ (less_dom (f,(R_EAL r))) = union (rng F) by MESFUNC1:21; hence Y /\ (less_dom (f,r)) = union (rng F) ; ::_thesis: verum end; theorem :: MESFUNC6:11 for X being non empty set for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) proof let X be non empty set ; ::_thesis: for Y being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) let Y be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,REAL for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) let f be PartFunc of X,REAL; ::_thesis: for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds Y /\ (great_dom (f,r)) = union (rng F) let r be Real; ::_thesis: ( ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) implies Y /\ (great_dom (f,r)) = union (rng F) ) assume for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ; ::_thesis: Y /\ (great_dom (f,r)) = union (rng F) then for n being Element of NAT holds F . n = Y /\ (great_eq_dom ((R_EAL f),(R_EAL (r + (1 / (n + 1)))))) ; then Y /\ (great_dom (f,(R_EAL r))) = union (rng F) by MESFUNC1:22; hence Y /\ (great_dom (f,r)) = union (rng F) ; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,REAL; let A be Element of S; predf is_measurable_on A means :Def1: :: MESFUNC6:def 1 R_EAL f is_measurable_on A; end; :: deftheorem Def1 defines is_measurable_on MESFUNC6:def_1_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff R_EAL f is_measurable_on A ); theorem Th12: :: MESFUNC6:12 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S ) let f be PartFunc of X,REAL; ::_thesis: for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S ) let A be Element of S; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S ) A1: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1; thus ( f is_measurable_on A implies for r being real number holds A /\ (less_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (less_dom (f,r)) in S ) implies f is_measurable_on A ) proof assume A2: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (less_dom (f,r)) in S let r be real number ; ::_thesis: A /\ (less_dom (f,r)) in S R_EAL r = r ; hence A /\ (less_dom (f,r)) in S by A1, A2, MESFUNC1:def_16; ::_thesis: verum end; ( ( for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S ) implies for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S ) ; hence ( ( for r being real number holds A /\ (less_dom (f,r)) in S ) implies f is_measurable_on A ) by A1, MESFUNC1:def_16; ::_thesis: verum end; theorem Th13: :: MESFUNC6:13 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) ) assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S ) A2: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1; thus ( f is_measurable_on A implies for r being real number holds A /\ (great_eq_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (great_eq_dom (f,r)) in S ) implies f is_measurable_on A ) proof assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_eq_dom (f,r)) in S let r be real number ; ::_thesis: A /\ (great_eq_dom (f,r)) in S A /\ (great_eq_dom (f,(R_EAL r))) in S by A1, A2, A3, MESFUNC1:27; hence A /\ (great_eq_dom (f,r)) in S ; ::_thesis: verum end; assume for r being real number holds A /\ (great_eq_dom (f,r)) in S ; ::_thesis: f is_measurable_on A then for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ; hence f is_measurable_on A by A1, A2, MESFUNC1:27; ::_thesis: verum end; theorem :: MESFUNC6:14 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S ) let f be PartFunc of X,REAL; ::_thesis: for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S ) let A be Element of S; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S ) A1: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1; thus ( f is_measurable_on A implies for r being real number holds A /\ (less_eq_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (less_eq_dom (f,r)) in S ) implies f is_measurable_on A ) proof assume A2: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (less_eq_dom (f,r)) in S let r be real number ; ::_thesis: A /\ (less_eq_dom (f,r)) in S R_EAL r = r ; hence A /\ (less_eq_dom (f,r)) in S by A1, A2, MESFUNC1:28; ::_thesis: verum end; assume for r being real number holds A /\ (less_eq_dom (f,r)) in S ; ::_thesis: f is_measurable_on A then for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ; hence f is_measurable_on A by A1, MESFUNC1:28; ::_thesis: verum end; theorem :: MESFUNC6:15 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) ) assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S ) A2: ( f is_measurable_on A iff R_EAL f is_measurable_on A ) by Def1; thus ( f is_measurable_on A implies for r being real number holds A /\ (great_dom (f,r)) in S ) ::_thesis: ( ( for r being real number holds A /\ (great_dom (f,r)) in S ) implies f is_measurable_on A ) proof assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_dom (f,r)) in S let r be real number ; ::_thesis: A /\ (great_dom (f,r)) in S A /\ (great_dom (f,(R_EAL r))) in S by A1, A2, A3, MESFUNC1:29; hence A /\ (great_dom (f,r)) in S ; ::_thesis: verum end; assume for r being real number holds A /\ (great_dom (f,r)) in S ; ::_thesis: f is_measurable_on A then for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ; hence f is_measurable_on A by A1, A2, MESFUNC1:29; ::_thesis: verum end; theorem :: MESFUNC6:16 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for B, A being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for B, A being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for B, A being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let B, A be Element of S; ::_thesis: ( B c= A & f is_measurable_on A implies f is_measurable_on B ) assume that A1: B c= A and A2: f is_measurable_on A ; ::_thesis: f is_measurable_on B R_EAL f is_measurable_on A by A2, Def1; then R_EAL f is_measurable_on B by A1, MESFUNC1:30; hence f is_measurable_on B by Def1; ::_thesis: verum end; theorem :: MESFUNC6:17 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let A, B be Element of S; ::_thesis: ( f is_measurable_on A & f is_measurable_on B implies f is_measurable_on A \/ B ) assume ( f is_measurable_on A & f is_measurable_on B ) ; ::_thesis: f is_measurable_on A \/ B then ( R_EAL f is_measurable_on A & R_EAL f is_measurable_on B ) by Def1; then R_EAL f is_measurable_on A \/ B by MESFUNC1:31; hence f is_measurable_on A \/ B by Def1; ::_thesis: verum end; theorem :: MESFUNC6:18 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S let f be PartFunc of X,REAL; ::_thesis: for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S let A be Element of S; ::_thesis: for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S let r, s be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S ) A1: ( R_EAL r = r & R_EAL s = s ) ; assume that A2: f is_measurable_on A and A3: A c= dom f ; ::_thesis: (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S R_EAL f is_measurable_on A by A2, Def1; hence (A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S by A1, A3, MESFUNC1:32; ::_thesis: verum end; theorem :: MESFUNC6:19 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S let r be Real; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S ) assume that A1: ( f is_measurable_on A & g is_measurable_on A ) and A2: A c= dom g ; ::_thesis: (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A1, Def1; then (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S by A2, MESFUNC1:36; hence (A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S ; ::_thesis: verum end; theorem Th20: :: MESFUNC6:20 for X being non empty set for f being PartFunc of X,REAL for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f) let f be PartFunc of X,REAL; ::_thesis: for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f) let r be Real; ::_thesis: R_EAL (r (#) f) = r (#) (R_EAL f) dom (R_EAL (r (#) f)) = dom (R_EAL f) by VALUED_1:def_5; then A1: dom (R_EAL (r (#) f)) = dom (r (#) (R_EAL f)) by MESFUNC1:def_6; now__::_thesis:_for_x_being_set_st_x_in_dom_(R_EAL_(r_(#)_f))_holds_ (R_EAL_(r_(#)_f))_._x_=_(r_(#)_(R_EAL_f))_._x let x be set ; ::_thesis: ( x in dom (R_EAL (r (#) f)) implies (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x ) assume A2: x in dom (R_EAL (r (#) f)) ; ::_thesis: (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x then (R_EAL (r (#) f)) . x = r * (f . x) by VALUED_1:def_5; then (R_EAL (r (#) f)) . x = (R_EAL r) * (R_EAL (f . x)) by EXTREAL1:1; hence (R_EAL (r (#) f)) . x = (r (#) (R_EAL f)) . x by A1, A2, MESFUNC1:def_6; ::_thesis: verum end; hence R_EAL (r (#) f) = r (#) (R_EAL f) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th21: :: MESFUNC6:21 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let r be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies r (#) f is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: r (#) f is_measurable_on A R_EAL f is_measurable_on A by A1, Def1; then r (#) (R_EAL f) is_measurable_on A by A2, MESFUNC1:37; then R_EAL (r (#) f) is_measurable_on A by Th20; hence r (#) f is_measurable_on A by Def1; ::_thesis: verum end; begin theorem :: MESFUNC6:22 for X being non empty set for f being PartFunc of X,REAL holds R_EAL f is V68() ; theorem Th23: :: MESFUNC6:23 for X being non empty set for f, g being PartFunc of X,REAL holds ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) let f, g be PartFunc of X,REAL; ::_thesis: ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) dom ((R_EAL f) - (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2; then A1: dom ((R_EAL f) - (R_EAL g)) = dom (f - g) by VALUED_1:12; A2: now__::_thesis:_for_x_being_set_st_x_in_dom_((R_EAL_f)_-_(R_EAL_g))_holds_ ((R_EAL_f)_-_(R_EAL_g))_._x_=_(f_-_g)_._x let x be set ; ::_thesis: ( x in dom ((R_EAL f) - (R_EAL g)) implies ((R_EAL f) - (R_EAL g)) . x = (f - g) . x ) assume A3: x in dom ((R_EAL f) - (R_EAL g)) ; ::_thesis: ((R_EAL f) - (R_EAL g)) . x = (f - g) . x then ((R_EAL f) - (R_EAL g)) . x = ((R_EAL f) . x) - ((R_EAL g) . x) by MESFUNC1:def_4 .= (f . x) - (g . x) by SUPINF_2:3 ; hence ((R_EAL f) - (R_EAL g)) . x = (f - g) . x by A1, A3, VALUED_1:13; ::_thesis: verum end; dom ((R_EAL f) + (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC2:2; then A4: dom ((R_EAL f) + (R_EAL g)) = dom (f + g) by VALUED_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_((R_EAL_f)_+_(R_EAL_g))_holds_ ((R_EAL_f)_+_(R_EAL_g))_._x_=_(f_+_g)_._x let x be set ; ::_thesis: ( x in dom ((R_EAL f) + (R_EAL g)) implies ((R_EAL f) + (R_EAL g)) . x = (f + g) . x ) assume A5: x in dom ((R_EAL f) + (R_EAL g)) ; ::_thesis: ((R_EAL f) + (R_EAL g)) . x = (f + g) . x then ((R_EAL f) + (R_EAL g)) . x = ((R_EAL f) . x) + ((R_EAL g) . x) by MESFUNC1:def_3 .= (f . x) + (g . x) by SUPINF_2:1 ; hence ((R_EAL f) + (R_EAL g)) . x = (f + g) . x by A4, A5, VALUED_1:def_1; ::_thesis: verum end; hence ( R_EAL (f + g) = (R_EAL f) + (R_EAL g) & R_EAL (f - g) = (R_EAL f) - (R_EAL g) & dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) ) by A4, A1, A2, FUNCT_1:2, MESFUNC2:2; ::_thesis: verum end; theorem :: MESFUNC6:24 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S for r being Real for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S for r being Real for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) let A be Element of S; ::_thesis: for r being Real for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) let r be Real; ::_thesis: for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds A /\ (less_dom ((f + g),r)) = union (rng F) let F be Function of RAT,S; ::_thesis: ( ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) ) assume for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: A /\ (less_dom ((f + g),r)) = union (rng F) then for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) ; then A1: A /\ (less_dom (((R_EAL f) + (R_EAL g)),(R_EAL r))) = union (rng F) by MESFUNC2:3; (R_EAL f) + (R_EAL g) = R_EAL (f + g) by Th23; hence A /\ (less_dom ((f + g),r)) = union (rng F) by A1; ::_thesis: verum end; theorem :: MESFUNC6:25 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & g is_measurable_on A holds ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) let r be Real; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) assume ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) then ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by Def1; then consider F being Function of RAT,S such that A1: for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by MESFUNC2:6; now__::_thesis:_for_p_being_Rational_holds_F_._p_=_(A_/\_(less_dom_(f,p)))_/\_(A_/\_(less_dom_(g,(r_-_p)))) let p be Rational; ::_thesis: F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) thus F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by A1 .= (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: verum end; hence ex F being Function of RAT,S st for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; ::_thesis: verum end; theorem Th26: :: MESFUNC6:26 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A holds f + g is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A implies f + g is_measurable_on A ) assume ( f is_measurable_on A & g is_measurable_on A ) ; ::_thesis: f + g is_measurable_on A then ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by Def1; then (R_EAL f) + (R_EAL g) is_measurable_on A by MESFUNC2:7; then R_EAL (f + g) is_measurable_on A by Th23; hence f + g is_measurable_on A by Def1; ::_thesis: verum end; theorem :: MESFUNC6:27 for X being non empty set for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) let f, g be PartFunc of X,REAL; ::_thesis: (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) (R_EAL f) - (R_EAL g) = R_EAL (f - g) by Th23 .= R_EAL (f + (- g)) ; hence (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g)) by Th23; ::_thesis: verum end; theorem Th28: :: MESFUNC6:28 for X being non empty set for f being PartFunc of X,REAL holds ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) ) let f be PartFunc of X,REAL; ::_thesis: ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) ) - (R_EAL f) = (- 1) (#) (R_EAL f) by MESFUNC2:9; hence ( - (R_EAL f) = R_EAL ((- 1) (#) f) & - (R_EAL f) = R_EAL (- f) ) by Th20; ::_thesis: verum end; theorem :: MESFUNC6:29 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & g is_measurable_on A & A c= dom g holds f - g is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies f - g is_measurable_on A ) assume that A1: f is_measurable_on A and A2: g is_measurable_on A and A3: A c= dom g ; ::_thesis: f - g is_measurable_on A R_EAL g is_measurable_on A by A2, Def1; then (- 1) (#) (R_EAL g) is_measurable_on A by A3, MESFUNC1:37; then - (R_EAL g) is_measurable_on A by MESFUNC2:9; then A4: R_EAL (- g) is_measurable_on A by Th28; R_EAL f is_measurable_on A by A1, Def1; then (R_EAL f) + (R_EAL (- g)) is_measurable_on A by A4, MESFUNC2:7; then R_EAL (f - g) is_measurable_on A by Th23; hence f - g is_measurable_on A by Def1; ::_thesis: verum end; begin theorem Th30: :: MESFUNC6:30 for X being non empty set for f being PartFunc of X,REAL holds ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f ) let f be PartFunc of X,REAL; ::_thesis: ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f ) A1: dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def_2 .= dom (max+ f) by RFUNCT_3:def_10 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(max+_(R_EAL_f))_holds_ (max+_(R_EAL_f))_._x_=_(max+_f)_._x let x be set ; ::_thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = (max+ f) . x ) assume A2: x in dom (max+ (R_EAL f)) ; ::_thesis: (max+ (R_EAL f)) . x = (max+ f) . x then (max+ (R_EAL f)) . x = max+ (f . x) by MESFUNC2:def_2; hence (max+ (R_EAL f)) . x = (max+ f) . x by A1, A2, RFUNCT_3:def_10; ::_thesis: verum end; hence max+ (R_EAL f) = max+ f by A1, FUNCT_1:2; ::_thesis: max- (R_EAL f) = max- f A3: dom (max- (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def_3 .= dom (max- f) by RFUNCT_3:def_11 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(max-_(R_EAL_f))_holds_ (max-_(R_EAL_f))_._x_=_(max-_f)_._x let x be set ; ::_thesis: ( x in dom (max- (R_EAL f)) implies (max- (R_EAL f)) . x = (max- f) . x ) assume A4: x in dom (max- (R_EAL f)) ; ::_thesis: (max- (R_EAL f)) . x = (max- f) . x then (max- (R_EAL f)) . x = max ((- (R_EAL (f . x))),0.) by MESFUNC2:def_3; then (max- (R_EAL f)) . x = max- (f . x) by SUPINF_2:2; hence (max- (R_EAL f)) . x = (max- f) . x by A3, A4, RFUNCT_3:def_11; ::_thesis: verum end; hence max- (R_EAL f) = max- f by A3, FUNCT_1:2; ::_thesis: verum end; theorem :: MESFUNC6:31 for X being non empty set for f being PartFunc of X,REAL for x being Element of X holds 0 <= (max+ f) . x proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being Element of X holds 0 <= (max+ f) . x let f be PartFunc of X,REAL; ::_thesis: for x being Element of X holds 0 <= (max+ f) . x let x be Element of X; ::_thesis: 0 <= (max+ f) . x 0. <= (max+ (R_EAL f)) . x by MESFUNC2:12; hence 0 <= (max+ f) . x by Th30; ::_thesis: verum end; theorem :: MESFUNC6:32 for X being non empty set for f being PartFunc of X,REAL for x being Element of X holds 0 <= (max- f) . x proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being Element of X holds 0 <= (max- f) . x let f be PartFunc of X,REAL; ::_thesis: for x being Element of X holds 0 <= (max- f) . x let x be Element of X; ::_thesis: 0 <= (max- f) . x 0. <= (max- (R_EAL f)) . x by MESFUNC2:13; hence 0 <= (max- f) . x by Th30; ::_thesis: verum end; theorem :: MESFUNC6:33 for X being non empty set for f being PartFunc of X,REAL holds max- f = max+ (- f) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds max- f = max+ (- f) let f be PartFunc of X,REAL; ::_thesis: max- f = max+ (- f) max- f = max- (R_EAL f) by Th30; then max- f = max+ (- (R_EAL f)) by MESFUNC2:14; then max- f = max+ (R_EAL (- f)) by Th28; hence max- f = max+ (- f) by Th30; ::_thesis: verum end; theorem :: MESFUNC6:34 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & 0 < (max+ f) . x holds (max- f) . x = 0 proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & 0 < (max+ f) . x holds (max- f) . x = 0 let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & 0 < (max+ f) . x holds (max- f) . x = 0 let x be set ; ::_thesis: ( x in dom f & 0 < (max+ f) . x implies (max- f) . x = 0 ) assume that A1: x in dom f and A2: 0 < (max+ f) . x ; ::_thesis: (max- f) . x = 0 0. < (max+ (R_EAL f)) . x by A2, Th30; then (max- (R_EAL f)) . x = 0. by A1, MESFUNC2:15; hence (max- f) . x = 0 by Th30; ::_thesis: verum end; theorem :: MESFUNC6:35 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & 0 < (max- f) . x holds (max+ f) . x = 0 proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & 0 < (max- f) . x holds (max+ f) . x = 0 let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & 0 < (max- f) . x holds (max+ f) . x = 0 let x be set ; ::_thesis: ( x in dom f & 0 < (max- f) . x implies (max+ f) . x = 0 ) assume that A1: x in dom f and A2: 0 < (max- f) . x ; ::_thesis: (max+ f) . x = 0 0. < (max- (R_EAL f)) . x by A2, Th30; then (max+ (R_EAL f)) . x = 0. by A1, MESFUNC2:16; hence (max+ f) . x = 0 by Th30; ::_thesis: verum end; theorem :: MESFUNC6:36 for X being non empty set for f being PartFunc of X,REAL holds ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) let f be PartFunc of X,REAL; ::_thesis: ( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) ) dom f = dom ((max+ (R_EAL f)) - (max- (R_EAL f))) by MESFUNC2:17; then dom f = dom ((R_EAL (max+ f)) - (max- (R_EAL f))) by Th30; then dom f = dom ((R_EAL (max+ f)) - (R_EAL (max- f))) by Th30; then dom f = dom (R_EAL ((max+ f) - (max- f))) by Th23; hence dom f = dom ((max+ f) - (max- f)) ; ::_thesis: dom f = dom ((max+ f) + (max- f)) dom f = dom ((max+ (R_EAL f)) + (max- (R_EAL f))) by MESFUNC2:17; then dom f = dom ((R_EAL (max+ f)) + (max- (R_EAL f))) by Th30; then dom f = dom ((R_EAL (max+ f)) + (R_EAL (max- f))) by Th30; then dom f = dom (R_EAL ((max+ f) + (max- f))) by Th23; hence dom f = dom ((max+ f) + (max- f)) ; ::_thesis: verum end; theorem :: MESFUNC6:37 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f holds ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) let x be set ; ::_thesis: ( x in dom f implies ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) ) A1: - ((R_EAL f) . x) = - (f . x) by SUPINF_2:2; assume A2: x in dom f ; ::_thesis: ( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ) then ( (max+ (R_EAL f)) . x = (R_EAL f) . x or (max+ (R_EAL f)) . x = 0. ) by MESFUNC2:18; hence ( (max+ f) . x = f . x or (max+ f) . x = 0 ) by Th30; ::_thesis: ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) ( (max- (R_EAL f)) . x = - ((R_EAL f) . x) or (max- (R_EAL f)) . x = 0. ) by A2, MESFUNC2:18; hence ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) by A1, Th30; ::_thesis: verum end; theorem :: MESFUNC6:38 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & (max+ f) . x = f . x holds (max- f) . x = 0 proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & (max+ f) . x = f . x holds (max- f) . x = 0 let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max+ f) . x = f . x holds (max- f) . x = 0 let x be set ; ::_thesis: ( x in dom f & (max+ f) . x = f . x implies (max- f) . x = 0 ) assume that A1: x in dom f and A2: (max+ f) . x = f . x ; ::_thesis: (max- f) . x = 0 R_EAL (f . x) = (max+ (R_EAL f)) . x by A2, Th30; then (max- (R_EAL f)) . x = 0. by A1, MESFUNC2:19; hence (max- f) . x = 0 by Th30; ::_thesis: verum end; theorem :: MESFUNC6:39 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & (max+ f) . x = 0 holds (max- f) . x = - (f . x) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & (max+ f) . x = 0 holds (max- f) . x = - (f . x) let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max+ f) . x = 0 holds (max- f) . x = - (f . x) let x be set ; ::_thesis: ( x in dom f & (max+ f) . x = 0 implies (max- f) . x = - (f . x) ) assume that A1: x in dom f and A2: (max+ f) . x = 0 ; ::_thesis: (max- f) . x = - (f . x) R_EAL 0 = (max+ (R_EAL f)) . x by A2, Th30; then (max- (R_EAL f)) . x = - ((R_EAL f) . x) by A1, MESFUNC2:20; then (max- f) . x = - ((R_EAL f) . x) by Th30; hence (max- f) . x = - (f . x) by SUPINF_2:2; ::_thesis: verum end; theorem :: MESFUNC6:40 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & (max- f) . x = - (f . x) holds (max+ f) . x = 0 proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & (max- f) . x = - (f . x) holds (max+ f) . x = 0 let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max- f) . x = - (f . x) holds (max+ f) . x = 0 let x be set ; ::_thesis: ( x in dom f & (max- f) . x = - (f . x) implies (max+ f) . x = 0 ) assume that A1: x in dom f and A2: (max- f) . x = - (f . x) ; ::_thesis: (max+ f) . x = 0 - (f . x) = (max- (R_EAL f)) . x by A2, Th30; then - ((R_EAL f) . x) = (max- (R_EAL f)) . x by SUPINF_2:2; then (max+ (R_EAL f)) . x = 0. by A1, MESFUNC2:21; hence (max+ f) . x = 0 by Th30; ::_thesis: verum end; theorem :: MESFUNC6:41 for X being non empty set for f being PartFunc of X,REAL for x being set st x in dom f & (max- f) . x = 0 holds (max+ f) . x = f . x proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for x being set st x in dom f & (max- f) . x = 0 holds (max+ f) . x = f . x let f be PartFunc of X,REAL; ::_thesis: for x being set st x in dom f & (max- f) . x = 0 holds (max+ f) . x = f . x let x be set ; ::_thesis: ( x in dom f & (max- f) . x = 0 implies (max+ f) . x = f . x ) assume that A1: x in dom f and A2: (max- f) . x = 0 ; ::_thesis: (max+ f) . x = f . x R_EAL 0 = (max- (R_EAL f)) . x by A2, Th30; then (max+ (R_EAL f)) . x = (R_EAL f) . x by A1, MESFUNC2:22; hence (max+ f) . x = f . x by Th30; ::_thesis: verum end; theorem :: MESFUNC6:42 for X being non empty set for f being PartFunc of X,REAL holds f = (max+ f) - (max- f) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds f = (max+ f) - (max- f) let f be PartFunc of X,REAL; ::_thesis: f = (max+ f) - (max- f) f = (max+ (R_EAL f)) - (max- (R_EAL f)) by MESFUNC2:23; then f = (R_EAL (max+ f)) - (max- (R_EAL f)) by Th30; then f = (R_EAL (max+ f)) - (R_EAL (max- f)) by Th30; then f = R_EAL ((max+ f) - (max- f)) by Th23; hence f = (max+ f) - (max- f) ; ::_thesis: verum end; theorem Th43: :: MESFUNC6:43 for r being Real holds |.r.| = |.(R_EAL r).| proof let r be Real; ::_thesis: |.r.| = |.(R_EAL r).| percases ( 0 <= r or r < 0 ) ; supposeA1: 0 <= r ; ::_thesis: |.r.| = |.(R_EAL r).| then |.(R_EAL r).| = R_EAL r by EXTREAL1:def_1; hence |.r.| = |.(R_EAL r).| by A1, ABSVALUE:def_1; ::_thesis: verum end; supposeA2: r < 0 ; ::_thesis: |.r.| = |.(R_EAL r).| then |.(R_EAL r).| = - (R_EAL r) by EXTREAL1:def_1; then |.(R_EAL r).| = R_EAL (- r) by SUPINF_2:2; hence |.r.| = |.(R_EAL r).| by A2, ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem Th44: :: MESFUNC6:44 for X being non empty set for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).| proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).| let f be PartFunc of X,REAL; ::_thesis: R_EAL (abs f) = |.(R_EAL f).| A1: dom (R_EAL (abs f)) = dom f by VALUED_1:def_11 .= dom |.(R_EAL f).| by MESFUNC1:def_10 ; now__::_thesis:_for_x_being_set_st_x_in_dom_(R_EAL_(abs_f))_holds_ (R_EAL_(abs_f))_._x_=_|.(R_EAL_f).|_._x let x be set ; ::_thesis: ( x in dom (R_EAL (abs f)) implies (R_EAL (abs f)) . x = |.(R_EAL f).| . x ) (R_EAL (abs f)) . x = |.(f . x).| by VALUED_1:18; then A2: (R_EAL (abs f)) . x = |.(R_EAL (f . x)).| by Th43; assume x in dom (R_EAL (abs f)) ; ::_thesis: (R_EAL (abs f)) . x = |.(R_EAL f).| . x hence (R_EAL (abs f)) . x = |.(R_EAL f).| . x by A1, A2, MESFUNC1:def_10; ::_thesis: verum end; hence R_EAL (abs f) = |.(R_EAL f).| by A1, FUNCT_1:2; ::_thesis: verum end; theorem :: MESFUNC6:45 for X being non empty set for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f) let f be PartFunc of X,REAL; ::_thesis: abs f = (max+ f) + (max- f) abs f = R_EAL (abs f) ; then abs f = |.(R_EAL f).| by Th44; then abs f = (max+ (R_EAL f)) + (max- (R_EAL f)) by MESFUNC2:24; then abs f = (R_EAL (max+ f)) + (max- (R_EAL f)) by Th30; then abs f = (R_EAL (max+ f)) + (R_EAL (max- f)) by Th30; then abs f = R_EAL ((max+ f) + (max- f)) by Th23; hence abs f = (max+ f) + (max- f) ; ::_thesis: verum end; begin theorem Th46: :: MESFUNC6:46 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A holds max+ f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A implies max+ f is_measurable_on A ) assume f is_measurable_on A ; ::_thesis: max+ f is_measurable_on A then R_EAL f is_measurable_on A by Def1; then max+ (R_EAL f) is_measurable_on A by MESFUNC2:25; then R_EAL (max+ f) is_measurable_on A by Th30; hence max+ f is_measurable_on A by Def1; ::_thesis: verum end; theorem Th47: :: MESFUNC6:47 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds max- f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies max- f is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: max- f is_measurable_on A R_EAL f is_measurable_on A by A1, Def1; then max- (R_EAL f) is_measurable_on A by A2, MESFUNC2:26; then R_EAL (max- f) is_measurable_on A by Th30; hence max- f is_measurable_on A by Def1; ::_thesis: verum end; theorem :: MESFUNC6:48 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds abs f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds abs f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_measurable_on A & A c= dom f holds abs f is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds abs f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies abs f is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: abs f is_measurable_on A R_EAL f is_measurable_on A by A1, Def1; then |.(R_EAL f).| is_measurable_on A by A2, MESFUNC2:27; then R_EAL (abs f) is_measurable_on A by Th44; hence abs f is_measurable_on A by Def1; ::_thesis: verum end; begin definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,REAL; predf is_simple_func_in S means :Def2: :: MESFUNC6:def 2 ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ); end; :: deftheorem Def2 defines is_simple_func_in MESFUNC6:def_2_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) ); theorem Th49: :: MESFUNC6:49 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL holds ( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL holds ( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL holds ( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) hereby ::_thesis: ( R_EAL f is_simple_func_in S implies f is_simple_func_in S ) assume f is_simple_func_in S ; ::_thesis: R_EAL f is_simple_func_in S then ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) by Def2; hence R_EAL f is_simple_func_in S by MESFUNC2:def_4; ::_thesis: verum end; assume R_EAL f is_simple_func_in S ; ::_thesis: f is_simple_func_in S then ex F being Finite_Sep_Sequence of S st ( dom (R_EAL f) = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (R_EAL f) . x = (R_EAL f) . y ) ) by MESFUNC2:def_4; hence f is_simple_func_in S by Def2; ::_thesis: verum end; theorem :: MESFUNC6:50 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_simple_func_in S holds f is_measurable_on A let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f is_measurable_on A ) assume f is_simple_func_in S ; ::_thesis: f is_measurable_on A then R_EAL f is_simple_func_in S by Th49; then R_EAL f is_measurable_on A by MESFUNC2:34; hence f is_measurable_on A by Def1; ::_thesis: verum end; theorem Th51: :: MESFUNC6:51 for X being set for f being PartFunc of X,REAL holds ( f is nonnegative iff for x being set holds 0 <= f . x ) proof let X be set ; ::_thesis: for f being PartFunc of X,REAL holds ( f is nonnegative iff for x being set holds 0 <= f . x ) let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative iff for x being set holds 0 <= f . x ) hereby ::_thesis: ( ( for x being set holds 0 <= f . x ) implies f is nonnegative ) assume f is nonnegative ; ::_thesis: for x being set holds 0 <= f . x then A1: rng f is nonnegative by SUPINF_2:def_16; hereby ::_thesis: verum let x be set ; ::_thesis: 0 <= f . x now__::_thesis:_(_x_in_dom_f_implies_0_<=_f_._x_) assume x in dom f ; ::_thesis: 0 <= f . x then A2: f . x in rng f by FUNCT_1:def_3; f . x in REAL ; hence 0 <= f . x by A1, A2, NUMBERS:31, SUPINF_2:def_9; ::_thesis: verum end; hence 0 <= f . x by FUNCT_1:def_2; ::_thesis: verum end; end; assume A3: for x being set holds 0 <= f . x ; ::_thesis: f is nonnegative let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not y in rng f or 0. <= y ) assume y in rng f ; ::_thesis: 0. <= y then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence 0. <= y by A3; ::_thesis: verum end; theorem Th52: :: MESFUNC6:52 for X being set for f being PartFunc of X,REAL st ( for x being set st x in dom f holds 0 <= f . x ) holds f is nonnegative proof let X be set ; ::_thesis: for f being PartFunc of X,REAL st ( for x being set st x in dom f holds 0 <= f . x ) holds f is nonnegative let f be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds 0 <= f . x ) implies f is nonnegative ) assume A1: for x being set st x in dom f holds 0 <= f . x ; ::_thesis: f is nonnegative let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not y in rng f or 0. <= y ) assume y in rng f ; ::_thesis: 0. <= y then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence 0. <= y by A1; ::_thesis: verum end; theorem :: MESFUNC6:53 for X being set for f being PartFunc of X,REAL holds ( f is nonpositive iff for x being set holds f . x <= 0 ) proof let X be set ; ::_thesis: for f being PartFunc of X,REAL holds ( f is nonpositive iff for x being set holds f . x <= 0 ) let f be PartFunc of X,REAL; ::_thesis: ( f is nonpositive iff for x being set holds f . x <= 0 ) hereby ::_thesis: ( ( for x being set holds f . x <= 0 ) implies f is nonpositive ) assume f is nonpositive ; ::_thesis: for x being set holds f . x <= 0 then A1: rng f is nonpositive by MESFUNC5:def_2; hereby ::_thesis: verum let x be set ; ::_thesis: f . x <= 0 now__::_thesis:_(_x_in_dom_f_implies_f_._x_<=_0_) assume x in dom f ; ::_thesis: f . x <= 0 then A2: f . x in rng f by FUNCT_1:def_3; f . x in REAL ; hence f . x <= 0 by A1, A2, MESFUNC5:def_1, NUMBERS:31; ::_thesis: verum end; hence f . x <= 0 by FUNCT_1:def_2; ::_thesis: verum end; end; assume A3: for x being set holds f . x <= 0 ; ::_thesis: f is nonpositive let y be R_eal; :: according to MESFUNC5:def_1,MESFUNC5:def_2 ::_thesis: ( not y in rng f or y <= 0 ) assume y in rng f ; ::_thesis: y <= 0 then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence y <= 0 by A3; ::_thesis: verum end; theorem Th54: :: MESFUNC6:54 for X being non empty set for f being PartFunc of X,REAL st ( for x being set st x in dom f holds f . x <= 0 ) holds f is nonpositive proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL st ( for x being set st x in dom f holds f . x <= 0 ) holds f is nonpositive let f be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds f . x <= 0 ) implies f is nonpositive ) assume A1: for x being set st x in dom f holds f . x <= 0 ; ::_thesis: f is nonpositive let y be R_eal; :: according to MESFUNC5:def_1,MESFUNC5:def_2 ::_thesis: ( not y in rng f or y <= 0 ) assume y in rng f ; ::_thesis: y <= 0 then ex x being set st ( x in dom f & y = f . x ) by FUNCT_1:def_3; hence y <= 0 by A1; ::_thesis: verum end; theorem :: MESFUNC6:55 for X being non empty set for Y being set for f being PartFunc of X,REAL st f is nonnegative holds f | Y is nonnegative proof let X be non empty set ; ::_thesis: for Y being set for f being PartFunc of X,REAL st f is nonnegative holds f | Y is nonnegative let Y be set ; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative holds f | Y is nonnegative let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative implies f | Y is nonnegative ) assume f is nonnegative ; ::_thesis: f | Y is nonnegative then A1: rng f is nonnegative by SUPINF_2:def_16; now__::_thesis:_for_y_being_R_eal_st_y_in_rng_(f_|_Y)_holds_ 0._<=_y let y be R_eal; ::_thesis: ( y in rng (f | Y) implies 0. <= y ) assume y in rng (f | Y) ; ::_thesis: 0. <= y then consider x being set such that A2: x in dom (f | Y) and A3: (f | Y) . x = y by FUNCT_1:def_3; x in (dom f) /\ Y by A2, RELAT_1:61; then A4: x in dom f by XBOOLE_0:def_4; (f | Y) . x = f . x by A2, FUNCT_1:47; then (f | Y) . x in rng f by A4, FUNCT_1:3; hence 0. <= y by A1, A3, SUPINF_2:def_9; ::_thesis: verum end; then rng (f | Y) is nonnegative by SUPINF_2:def_9; hence f | Y is nonnegative by SUPINF_2:def_16; ::_thesis: verum end; theorem Th56: :: MESFUNC6:56 for X being non empty set for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds f + g is nonnegative proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st f is nonnegative & g is nonnegative holds f + g is nonnegative let f, g be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & g is nonnegative implies f + g is nonnegative ) assume that A1: f is nonnegative and A2: g is nonnegative ; ::_thesis: f + g is nonnegative for x being set st x in dom (f + g) holds 0 <= (f + g) . x proof let x be set ; ::_thesis: ( x in dom (f + g) implies 0 <= (f + g) . x ) assume A3: x in dom (f + g) ; ::_thesis: 0 <= (f + g) . x 0 <= f . x by A1, Th51; then A4: g . x <= (f . x) + (g . x) by XREAL_1:31; 0 <= g . x by A2, Th51; hence 0 <= (f + g) . x by A3, A4, VALUED_1:def_1; ::_thesis: verum end; hence f + g is nonnegative by Th52; ::_thesis: verum end; theorem :: MESFUNC6:57 for X being non empty set for f being PartFunc of X,REAL for r being Real st f is nonnegative holds ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real st f is nonnegative holds ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is nonnegative holds ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) let r be Real; ::_thesis: ( f is nonnegative implies ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) ) assume A1: f is nonnegative ; ::_thesis: ( ( 0 <= r implies r (#) f is nonnegative ) & ( r <= 0 implies r (#) f is nonpositive ) ) hereby ::_thesis: ( r <= 0 implies r (#) f is nonpositive ) assume A2: 0 <= r ; ::_thesis: r (#) f is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_f)_holds_ 0_<=_(r_(#)_f)_._x let x be set ; ::_thesis: ( x in dom (r (#) f) implies 0 <= (r (#) f) . x ) assume A3: x in dom (r (#) f) ; ::_thesis: 0 <= (r (#) f) . x 0 <= f . x by A1, Th51; then 0 * r <= r * (f . x) by A2; hence 0 <= (r (#) f) . x by A3, VALUED_1:def_5; ::_thesis: verum end; hence r (#) f is nonnegative by Th52; ::_thesis: verum end; assume A4: r <= 0 ; ::_thesis: r (#) f is nonpositive now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_f)_holds_ (r_(#)_f)_._x_<=_0 let x be set ; ::_thesis: ( x in dom (r (#) f) implies (r (#) f) . x <= 0 ) assume A5: x in dom (r (#) f) ; ::_thesis: (r (#) f) . x <= 0 0 <= f . x by A1, Th51; then r * (f . x) <= r * 0 by A4; hence (r (#) f) . x <= 0 by A5, VALUED_1:def_5; ::_thesis: verum end; hence r (#) f is nonpositive by Th54; ::_thesis: verum end; theorem Th58: :: MESFUNC6:58 for X being non empty set for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds g . x <= f . x ) holds f - g is nonnegative proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds g . x <= f . x ) holds f - g is nonnegative let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in (dom f) /\ (dom g) holds g . x <= f . x ) implies f - g is nonnegative ) assume A1: for x being set st x in (dom f) /\ (dom g) holds g . x <= f . x ; ::_thesis: f - g is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_(f_-_g)_holds_ 0_<=_(f_-_g)_._x let x be set ; ::_thesis: ( x in dom (f - g) implies 0 <= (f - g) . x ) assume A2: x in dom (f - g) ; ::_thesis: 0 <= (f - g) . x dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12; then 0 <= (f . x) - (g . x) by A1, A2, XREAL_1:48; hence 0 <= (f - g) . x by A2, VALUED_1:13; ::_thesis: verum end; hence f - g is nonnegative by Th52; ::_thesis: verum end; theorem :: MESFUNC6:59 for X being non empty set for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds (f + g) + h is nonnegative proof let X be non empty set ; ::_thesis: for f, g, h being PartFunc of X,REAL st f is nonnegative & g is nonnegative & h is nonnegative holds (f + g) + h is nonnegative let f, g, h be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & g is nonnegative & h is nonnegative implies (f + g) + h is nonnegative ) assume that A1: ( f is nonnegative & g is nonnegative ) and A2: h is nonnegative ; ::_thesis: (f + g) + h is nonnegative f + g is nonnegative by A1, Th56; hence (f + g) + h is nonnegative by A2, Th56; ::_thesis: verum end; theorem Th60: :: MESFUNC6:60 for X being non empty set for f, g, h being PartFunc of X,REAL for x being set st x in dom ((f + g) + h) holds ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) proof let X be non empty set ; ::_thesis: for f, g, h being PartFunc of X,REAL for x being set st x in dom ((f + g) + h) holds ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) let f, g, h be PartFunc of X,REAL; ::_thesis: for x being set st x in dom ((f + g) + h) holds ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) let x be set ; ::_thesis: ( x in dom ((f + g) + h) implies ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) ) assume A1: x in dom ((f + g) + h) ; ::_thesis: ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) dom ((f + g) + h) = (dom (f + g)) /\ (dom h) by VALUED_1:def_1; then x in dom (f + g) by A1, XBOOLE_0:def_4; then ((f . x) + (g . x)) + (h . x) = ((f + g) . x) + (h . x) by VALUED_1:def_1; hence ((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) by A1, VALUED_1:def_1; ::_thesis: verum end; theorem :: MESFUNC6:61 for X being non empty set for f being PartFunc of X,REAL holds ( max+ f is nonnegative & max- f is nonnegative ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds ( max+ f is nonnegative & max- f is nonnegative ) let f be PartFunc of X,REAL; ::_thesis: ( max+ f is nonnegative & max- f is nonnegative ) for x being set st x in dom (max+ f) holds 0 <= (max+ f) . x by RFUNCT_3:37; hence max+ f is nonnegative by Th52; ::_thesis: max- f is nonnegative for x being set st x in dom (max- f) holds 0 <= (max- f) . x by RFUNCT_3:40; hence max- f is nonnegative by Th52; ::_thesis: verum end; theorem Th62: :: MESFUNC6:62 for X being non empty set for f, g being PartFunc of X,REAL holds ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) let f, g be PartFunc of X,REAL; ::_thesis: ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) A1: ( dom (max- f) = dom f & dom ((max+ (f + g)) + (max- f)) = (dom (max+ (f + g))) /\ (dom (max- f)) ) by RFUNCT_3:def_11, VALUED_1:def_1; A2: ( dom (max+ f) = dom f & dom ((max- (f + g)) + (max+ f)) = (dom (max- (f + g))) /\ (dom (max+ f)) ) by RFUNCT_3:def_10, VALUED_1:def_1; A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; then A4: dom (max- (f + g)) = (dom f) /\ (dom g) by RFUNCT_3:def_11; dom (max+ (f + g)) = (dom f) /\ (dom g) by A3, RFUNCT_3:def_10; then A5: dom ((max+ (f + g)) + (max- f)) = (dom g) /\ ((dom f) /\ (dom f)) by A1, XBOOLE_1:16; hence ( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) ) by A4, A2, XBOOLE_1:16; ::_thesis: ( dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) dom (max- g) = dom g by RFUNCT_3:def_11; then dom (((max+ (f + g)) + (max- f)) + (max- g)) = ((dom f) /\ (dom g)) /\ (dom g) by A5, VALUED_1:def_1 .= (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16 ; hence dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) ; ::_thesis: ( dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) ( dom (max+ g) = dom g & dom ((max- (f + g)) + (max+ f)) = (dom g) /\ ((dom f) /\ (dom f)) ) by A4, A2, RFUNCT_3:def_10, XBOOLE_1:16; then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = ((dom f) /\ (dom g)) /\ (dom g) by VALUED_1:def_1; then dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ ((dom g) /\ (dom g)) by XBOOLE_1:16; hence dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) ; ::_thesis: ( (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative ) now__::_thesis:_for_x_being_set_st_x_in_dom_((max+_(f_+_g))_+_(max-_f))_holds_ 0_<=_((max+_(f_+_g))_+_(max-_f))_._x let x be set ; ::_thesis: ( x in dom ((max+ (f + g)) + (max- f)) implies 0 <= ((max+ (f + g)) + (max- f)) . x ) assume A6: x in dom ((max+ (f + g)) + (max- f)) ; ::_thesis: 0 <= ((max+ (f + g)) + (max- f)) . x then ( 0 <= (max+ (f + g)) . x & 0 <= (max- f) . x ) by RFUNCT_3:37, RFUNCT_3:40; then 0 + 0 <= ((max+ (f + g)) . x) + ((max- f) . x) ; hence 0 <= ((max+ (f + g)) + (max- f)) . x by A6, VALUED_1:def_1; ::_thesis: verum end; hence (max+ (f + g)) + (max- f) is nonnegative by Th52; ::_thesis: (max- (f + g)) + (max+ f) is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_((max-_(f_+_g))_+_(max+_f))_holds_ 0_<=_((max-_(f_+_g))_+_(max+_f))_._x let x be set ; ::_thesis: ( x in dom ((max- (f + g)) + (max+ f)) implies 0 <= ((max- (f + g)) + (max+ f)) . x ) assume A7: x in dom ((max- (f + g)) + (max+ f)) ; ::_thesis: 0 <= ((max- (f + g)) + (max+ f)) . x then ( 0 <= (max- (f + g)) . x & 0 <= (max+ f) . x ) by RFUNCT_3:37, RFUNCT_3:40; then 0 + 0 <= ((max- (f + g)) . x) + ((max+ f) . x) ; hence 0 <= ((max- (f + g)) + (max+ f)) . x by A7, VALUED_1:def_1; ::_thesis: verum end; hence (max- (f + g)) + (max+ f) is nonnegative by Th52; ::_thesis: verum end; theorem :: MESFUNC6:63 for X being non empty set for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) let f, g be PartFunc of X,REAL; ::_thesis: ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) A1: dom (max+ (f + g)) = dom (f + g) by RFUNCT_3:def_10; A2: dom (max+ g) = dom g by RFUNCT_3:def_10; A3: dom (max+ f) = dom f by RFUNCT_3:def_10; A4: dom (max- f) = dom f by RFUNCT_3:def_11; A5: dom (max- g) = dom g by RFUNCT_3:def_11; A6: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom ((max+ (f + g)) + (max- f))) /\ (dom (max- g)) by VALUED_1:def_1 .= ((dom (f + g)) /\ (dom f)) /\ (dom g) by A1, A4, A5, VALUED_1:def_1 ; then A7: dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom (f + g)) /\ ((dom f) /\ (dom g)) by XBOOLE_1:16; A8: dom (max- (f + g)) = dom (f + g) by RFUNCT_3:def_11; A9: for x being set st x in dom (((max+ (f + g)) + (max- f)) + (max- g)) holds (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x proof let x be set ; ::_thesis: ( x in dom (((max+ (f + g)) + (max- f)) + (max- g)) implies (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x ) assume A10: x in dom (((max+ (f + g)) + (max- f)) + (max- g)) ; ::_thesis: (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x then A11: x in dom g by A6, XBOOLE_0:def_4; then A12: (max+ g) . x = max+ (g . x) by A2, RFUNCT_3:def_10; A13: (max- g) . x = max- (g . x) by A5, A11, RFUNCT_3:def_11; A14: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; then A15: (max+ (f + g)) . x = max+ ((f + g) . x) by A1, A7, A10, RFUNCT_3:def_10 .= max (((f . x) + (g . x)),0) by A7, A10, A14, VALUED_1:def_1 ; A16: x in dom f by A7, A10, A14, XBOOLE_0:def_4; then A17: (max+ f) . x = max+ (f . x) by A3, RFUNCT_3:def_10; A18: (max- (f + g)) . x = max- ((f + g) . x) by A8, A7, A10, A14, RFUNCT_3:def_11 .= max ((- ((f . x) + (g . x))),0) by A7, A10, A14, VALUED_1:def_1 ; A19: (max- f) . x = max- (f . x) by A4, A16, RFUNCT_3:def_11; A20: now__::_thesis:_(_0_<=_f_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A21: 0 <= f . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then A22: (max- f) . x = 0 by A19, XXREAL_0:def_10; A23: now__::_thesis:_(_g_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A24: g . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then A25: (max- g) . x = - (g . x) by A13, XXREAL_0:def_10; A26: (max+ g) . x = 0 by A12, A24, XXREAL_0:def_10; A27: now__::_thesis:_(_(f_._x)_+_(g_._x)_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A28: (f . x) + (g . x) < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def_10; then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + (f . x)) + 0 by A17, A21, A26, XXREAL_0:def_10; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A22, A25, A28, XXREAL_0:def_10; ::_thesis: verum end; now__::_thesis:_(_0_<=_(f_._x)_+_(g_._x)_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume 0 <= (f . x) + (g . x) ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + 0) + (- (g . x)) ) by A15, A18, A22, A25, XXREAL_0:def_10; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A26, XXREAL_0:def_10; ::_thesis: verum end; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A27; ::_thesis: verum end; now__::_thesis:_(_0_<=_g_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A29: 0 <= g . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then (max- g) . x = 0 by A13, XXREAL_0:def_10; then A30: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (f . x) + (g . x) by A15, A21, A22, A29, XXREAL_0:def_10; ( (max- (f + g)) . x = 0 & (max+ g) . x = g . x ) by A18, A12, A21, A29, XXREAL_0:def_10; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A21, A30, XXREAL_0:def_10; ::_thesis: verum end; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A23; ::_thesis: verum end; A31: now__::_thesis:_(_f_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A32: f . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then A33: (max- f) . x = - (f . x) by A19, XXREAL_0:def_10; A34: now__::_thesis:_(_0_<=_g_._x_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A35: 0 <= g . x ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then A36: (max- g) . x = 0 by A13, XXREAL_0:def_10; A37: (max+ g) . x = g . x by A12, A35, XXREAL_0:def_10; A38: now__::_thesis:_(_(f_._x)_+_(g_._x)_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A39: (f . x) + (g . x) < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then (max- (f + g)) . x = - ((f . x) + (g . x)) by A18, XXREAL_0:def_10; then (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + (g . x) by A17, A32, A37, XXREAL_0:def_10 .= (- (f . x)) + ((- (g . x)) + (g . x)) ; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A15, A33, A36, A39, XXREAL_0:def_10; ::_thesis: verum end; now__::_thesis:_(_0_<=_(f_._x)_+_(g_._x)_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume 0 <= (f . x) + (g . x) ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then ( (max- (f + g)) . x = 0 & (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((f . x) + (g . x)) + (- (f . x))) + 0 ) by A15, A18, A33, A36, XXREAL_0:def_10; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A17, A32, A37, XXREAL_0:def_10; ::_thesis: verum end; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A38; ::_thesis: verum end; now__::_thesis:_(_g_._x_<_0_implies_(((max+_(f_+_g))_._x)_+_((max-_f)_._x))_+_((max-_g)_._x)_=_(((max-_(f_+_g))_._x)_+_((max+_f)_._x))_+_((max+_g)_._x)_) assume A40: g . x < 0 ; ::_thesis: (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) then ( (max- (f + g)) . x = - ((f . x) + (g . x)) & (max+ g) . x = 0 ) by A18, A12, A32, XXREAL_0:def_10; then A41: (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) = ((- ((f . x) + (g . x))) + 0) + 0 by A17, A32, XXREAL_0:def_10; (max- g) . x = - (g . x) by A13, A40, XXREAL_0:def_10; then (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (0 + (- (f . x))) + (- (g . x)) by A15, A32, A33, A40, XXREAL_0:def_10; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A41; ::_thesis: verum end; hence (((max+ (f + g)) . x) + ((max- f) . x)) + ((max- g) . x) = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by A34; ::_thesis: verum end; x in (dom f) /\ (dom g) by A10, Th62; then x in dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62; then (((max- (f + g)) + (max+ f)) + (max+ g)) . x = (((max- (f + g)) . x) + ((max+ f) . x)) + ((max+ g) . x) by Th60; hence (((max+ (f + g)) + (max- f)) + (max- g)) . x = (((max- (f + g)) + (max+ f)) + (max+ g)) . x by A10, A20, A31, Th60; ::_thesis: verum end; dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) by Th62; then dom (((max+ (f + g)) + (max- f)) + (max- g)) = dom (((max- (f + g)) + (max+ f)) + (max+ g)) by Th62; hence ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g) by A9, FUNCT_1:2; ::_thesis: verum end; theorem :: MESFUNC6:64 for X being non empty set for f being PartFunc of X,REAL for r being Real st 0 <= r holds ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real st 0 <= r holds ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real st 0 <= r holds ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) let r be Real; ::_thesis: ( 0 <= r implies ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) ) assume A1: 0 <= r ; ::_thesis: ( max+ (r (#) f) = r (#) (max+ f) & max- (r (#) f) = r (#) (max- f) ) A2: dom (max+ (r (#) f)) = dom (r (#) f) by RFUNCT_3:def_10 .= dom f by VALUED_1:def_5 .= dom (max+ f) by RFUNCT_3:def_10 .= dom (r (#) (max+ f)) by VALUED_1:def_5 ; for x being Element of X st x in dom (max+ (r (#) f)) holds (max+ (r (#) f)) . x = (r (#) (max+ f)) . x proof let x be Element of X; ::_thesis: ( x in dom (max+ (r (#) f)) implies (max+ (r (#) f)) . x = (r (#) (max+ f)) . x ) assume A3: x in dom (max+ (r (#) f)) ; ::_thesis: (max+ (r (#) f)) . x = (r (#) (max+ f)) . x then A4: x in dom (r (#) f) by RFUNCT_3:def_10; then x in dom f by VALUED_1:def_5; then A5: x in dom (max+ f) by RFUNCT_3:def_10; A6: (max+ (r (#) f)) . x = max+ ((r (#) f) . x) by A3, RFUNCT_3:def_10 .= max ((r * (f . x)),0) by A4, VALUED_1:def_5 ; (r (#) (max+ f)) . x = r * ((max+ f) . x) by A2, A3, VALUED_1:def_5 .= r * (max+ (f . x)) by A5, RFUNCT_3:def_10 .= max ((r * (f . x)),(r * 0)) by A1, FUZZY_2:41 ; hence (max+ (r (#) f)) . x = (r (#) (max+ f)) . x by A6; ::_thesis: verum end; hence max+ (r (#) f) = r (#) (max+ f) by A2, PARTFUN1:5; ::_thesis: max- (r (#) f) = r (#) (max- f) A7: dom (max- (r (#) f)) = dom (r (#) f) by RFUNCT_3:def_11 .= dom f by VALUED_1:def_5 .= dom (max- f) by RFUNCT_3:def_11 .= dom (r (#) (max- f)) by VALUED_1:def_5 ; for x being Element of X st x in dom (max- (r (#) f)) holds (max- (r (#) f)) . x = (r (#) (max- f)) . x proof let x be Element of X; ::_thesis: ( x in dom (max- (r (#) f)) implies (max- (r (#) f)) . x = (r (#) (max- f)) . x ) assume A8: x in dom (max- (r (#) f)) ; ::_thesis: (max- (r (#) f)) . x = (r (#) (max- f)) . x then A9: x in dom (r (#) f) by RFUNCT_3:def_11; then x in dom f by VALUED_1:def_5; then A10: x in dom (max- f) by RFUNCT_3:def_11; A11: (max- (r (#) f)) . x = max- ((r (#) f) . x) by A8, RFUNCT_3:def_11 .= max ((- (r * (f . x))),0) by A9, VALUED_1:def_5 ; (r (#) (max- f)) . x = r * ((max- f) . x) by A7, A8, VALUED_1:def_5 .= r * (max- (f . x)) by A10, RFUNCT_3:def_11 .= max ((r * (- (f . x))),(r * 0)) by A1, FUZZY_2:41 .= max ((- (r * (f . x))),(r * 0)) ; hence (max- (r (#) f)) . x = (r (#) (max- f)) . x by A11; ::_thesis: verum end; hence max- (r (#) f) = r (#) (max- f) by A7, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUNC6:65 for X being non empty set for f being PartFunc of X,REAL for r being Real st 0 <= r holds ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real st 0 <= r holds ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real st 0 <= r holds ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) let r be Real; ::_thesis: ( 0 <= r implies ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) ) assume A1: 0 <= r ; ::_thesis: ( max+ ((- r) (#) f) = r (#) (max- f) & max- ((- r) (#) f) = r (#) (max+ f) ) A2: dom (max+ ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def_10; then dom (max+ ((- r) (#) f)) = dom f by VALUED_1:def_5; then A3: dom (max+ ((- r) (#) f)) = dom (max- f) by RFUNCT_3:def_11; then A4: dom (max+ ((- r) (#) f)) = dom (r (#) (max- f)) by VALUED_1:def_5; for x being Element of X st x in dom (max+ ((- r) (#) f)) holds (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x proof let x be Element of X; ::_thesis: ( x in dom (max+ ((- r) (#) f)) implies (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x ) assume A5: x in dom (max+ ((- r) (#) f)) ; ::_thesis: (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x then A6: (max+ ((- r) (#) f)) . x = max+ (((- r) (#) f) . x) by RFUNCT_3:def_10 .= max (((- r) * (f . x)),0) by A2, A5, VALUED_1:def_5 ; (r (#) (max- f)) . x = r * ((max- f) . x) by A4, A5, VALUED_1:def_5 .= r * (max- (f . x)) by A3, A5, RFUNCT_3:def_11 .= max ((r * (- (f . x))),(r * 0)) by A1, FUZZY_2:41 ; hence (max+ ((- r) (#) f)) . x = (r (#) (max- f)) . x by A6; ::_thesis: verum end; hence max+ ((- r) (#) f) = r (#) (max- f) by A4, PARTFUN1:5; ::_thesis: max- ((- r) (#) f) = r (#) (max+ f) A7: dom (max- ((- r) (#) f)) = dom ((- r) (#) f) by RFUNCT_3:def_11; then dom (max- ((- r) (#) f)) = dom f by VALUED_1:def_5; then A8: dom (max- ((- r) (#) f)) = dom (max+ f) by RFUNCT_3:def_10; then A9: dom (max- ((- r) (#) f)) = dom (r (#) (max+ f)) by VALUED_1:def_5; for x being Element of X st x in dom (max- ((- r) (#) f)) holds (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x proof let x be Element of X; ::_thesis: ( x in dom (max- ((- r) (#) f)) implies (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x ) assume A10: x in dom (max- ((- r) (#) f)) ; ::_thesis: (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x then A11: (max- ((- r) (#) f)) . x = max- (((- r) (#) f) . x) by RFUNCT_3:def_11 .= max ((- ((- r) * (f . x))),0) by A7, A10, VALUED_1:def_5 ; (r (#) (max+ f)) . x = r * ((max+ f) . x) by A9, A10, VALUED_1:def_5 .= r * (max+ (f . x)) by A8, A10, RFUNCT_3:def_10 .= max ((r * (f . x)),(r * 0)) by A1, FUZZY_2:41 ; hence (max- ((- r) (#) f)) . x = (r (#) (max+ f)) . x by A11; ::_thesis: verum end; hence max- ((- r) (#) f) = r (#) (max+ f) by A9, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUNC6:66 for X being non empty set for Y being set for f being PartFunc of X,REAL holds ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y ) proof let X be non empty set ; ::_thesis: for Y being set for f being PartFunc of X,REAL holds ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y ) let Y be set ; ::_thesis: for f being PartFunc of X,REAL holds ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y ) let f be PartFunc of X,REAL; ::_thesis: ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y ) A1: dom (max+ (f | Y)) = dom (f | Y) by RFUNCT_3:def_10 .= (dom f) /\ Y by RELAT_1:61 .= (dom (max+ f)) /\ Y by RFUNCT_3:def_10 .= dom ((max+ f) | Y) by RELAT_1:61 ; for x being Element of X st x in dom (max+ (f | Y)) holds (max+ (f | Y)) . x = ((max+ f) | Y) . x proof let x be Element of X; ::_thesis: ( x in dom (max+ (f | Y)) implies (max+ (f | Y)) . x = ((max+ f) | Y) . x ) assume A2: x in dom (max+ (f | Y)) ; ::_thesis: (max+ (f | Y)) . x = ((max+ f) | Y) . x then A3: x in (dom (max+ f)) /\ Y by A1, RELAT_1:61; then A4: x in Y by XBOOLE_0:def_4; A5: x in dom (max+ f) by A3, XBOOLE_0:def_4; A6: (max+ (f | Y)) . x = max+ ((f | Y) . x) by A2, RFUNCT_3:def_10 .= max ((f . x),0) by A4, FUNCT_1:49 ; ((max+ f) | Y) . x = (max+ f) . x by A1, A2, FUNCT_1:47 .= max+ (f . x) by A5, RFUNCT_3:def_10 ; hence (max+ (f | Y)) . x = ((max+ f) | Y) . x by A6; ::_thesis: verum end; hence max+ (f | Y) = (max+ f) | Y by A1, PARTFUN1:5; ::_thesis: max- (f | Y) = (max- f) | Y A7: dom (max- (f | Y)) = dom (f | Y) by RFUNCT_3:def_11 .= (dom f) /\ Y by RELAT_1:61 .= (dom (max- f)) /\ Y by RFUNCT_3:def_11 .= dom ((max- f) | Y) by RELAT_1:61 ; for x being Element of X st x in dom (max- (f | Y)) holds (max- (f | Y)) . x = ((max- f) | Y) . x proof let x be Element of X; ::_thesis: ( x in dom (max- (f | Y)) implies (max- (f | Y)) . x = ((max- f) | Y) . x ) assume A8: x in dom (max- (f | Y)) ; ::_thesis: (max- (f | Y)) . x = ((max- f) | Y) . x then A9: x in (dom (max- f)) /\ Y by A7, RELAT_1:61; then A10: x in Y by XBOOLE_0:def_4; A11: x in dom (max- f) by A9, XBOOLE_0:def_4; A12: (max- (f | Y)) . x = max- ((f | Y) . x) by A8, RFUNCT_3:def_11 .= max ((- (f . x)),0) by A10, FUNCT_1:49 ; ((max- f) | Y) . x = (max- f) . x by A7, A8, FUNCT_1:47 .= max- (f . x) by A11, RFUNCT_3:def_11 ; hence (max- (f | Y)) . x = ((max- f) | Y) . x by A12; ::_thesis: verum end; hence max- (f | Y) = (max- f) | Y by A7, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUNC6:67 for X being non empty set for Y being set for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) proof let X be non empty set ; ::_thesis: for Y being set for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) let Y be set ; ::_thesis: for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) let f, g be PartFunc of X,REAL; ::_thesis: ( Y c= dom (f + g) implies ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) ) assume A1: Y c= dom (f + g) ; ::_thesis: ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) (dom (f | Y)) /\ (dom (g | Y)) = ((dom f) /\ Y) /\ (dom (g | Y)) by RELAT_1:61 .= ((dom f) /\ Y) /\ ((dom g) /\ Y) by RELAT_1:61 .= (((dom f) /\ Y) /\ (dom g)) /\ Y by XBOOLE_1:16 .= (((dom f) /\ (dom g)) /\ Y) /\ Y by XBOOLE_1:16 .= ((dom f) /\ (dom g)) /\ (Y /\ Y) by XBOOLE_1:16 ; then A2: dom ((f | Y) + (g | Y)) = ((dom f) /\ (dom g)) /\ Y by VALUED_1:def_1 .= (dom (f + g)) /\ Y by VALUED_1:def_1 .= Y by A1, XBOOLE_1:28 ; A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; dom (g | Y) = (dom g) /\ Y by RELAT_1:61; then A4: dom (g | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28; A5: dom ((f + g) | Y) = (dom (f + g)) /\ Y by RELAT_1:61; then A6: dom ((f + g) | Y) = Y by A1, XBOOLE_1:28; dom (f | Y) = (dom f) /\ Y by RELAT_1:61; then A7: dom (f | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28; now__::_thesis:_for_x_being_set_st_x_in_dom_((f_+_g)_|_Y)_holds_ ((f_+_g)_|_Y)_._x_=_((f_|_Y)_+_(g_|_Y))_._x let x be set ; ::_thesis: ( x in dom ((f + g) | Y) implies ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x ) assume A8: x in dom ((f + g) | Y) ; ::_thesis: ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x hence ((f + g) | Y) . x = (f + g) . x by FUNCT_1:47 .= (f . x) + (g . x) by A1, A6, A8, VALUED_1:def_1 .= ((f | Y) . x) + (g . x) by A6, A7, A8, FUNCT_1:47 .= ((f | Y) . x) + ((g | Y) . x) by A6, A4, A8, FUNCT_1:47 .= ((f | Y) + (g | Y)) . x by A6, A2, A8, VALUED_1:def_1 ; ::_thesis: verum end; hence ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A1, A5, A2, FUNCT_1:2, XBOOLE_1:28; ::_thesis: verum end; theorem :: MESFUNC6:68 for X being non empty set for f being PartFunc of X,REAL for r being Real holds eq_dom (f,r) = f " {r} proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for r being Real holds eq_dom (f,r) = f " {r} let f be PartFunc of X,REAL; ::_thesis: for r being Real holds eq_dom (f,r) = f " {r} let r be Real; ::_thesis: eq_dom (f,r) = f " {r} now__::_thesis:_for_x_being_set_st_x_in_f_"_{r}_holds_ x_in_eq_dom_(f,r) let x be set ; ::_thesis: ( x in f " {r} implies x in eq_dom (f,r) ) assume A1: x in f " {r} ; ::_thesis: x in eq_dom (f,r) then f . x in {r} by FUNCT_1:def_7; then A2: (R_EAL f) . x = R_EAL r by TARSKI:def_1; x in dom f by A1, FUNCT_1:def_7; hence x in eq_dom (f,r) by A2, MESFUNC1:def_15; ::_thesis: verum end; then A3: f " {r} c= eq_dom (f,r) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_eq_dom_(f,r)_holds_ x_in_f_"_{r} let x be set ; ::_thesis: ( x in eq_dom (f,r) implies x in f " {r} ) assume A4: x in eq_dom (f,r) ; ::_thesis: x in f " {r} then r = f . x by MESFUNC1:def_15; then A5: f . x in {r} by TARSKI:def_1; x in dom f by A4, MESFUNC1:def_15; hence x in f " {r} by A5, FUNCT_1:def_7; ::_thesis: verum end; then eq_dom (f,r) c= f " {r} by TARSKI:def_3; hence eq_dom (f,r) = f " {r} by A3, XBOOLE_0:def_10; ::_thesis: verum end; begin theorem :: MESFUNC6:69 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S let f be PartFunc of X,REAL; ::_thesis: for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S let A be Element of S; ::_thesis: for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S let r, s be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S R_EAL f is_measurable_on A by A1, Def1; then A3: A /\ (less_dom ((R_EAL f),(R_EAL s))) in S by MESFUNC1:def_16; A4: (A /\ (great_eq_dom (f,r))) /\ (A /\ (less_dom (f,s))) = ((A /\ (great_eq_dom (f,r))) /\ A) /\ (less_dom (f,s)) by XBOOLE_1:16 .= ((great_eq_dom (f,r)) /\ (A /\ A)) /\ (less_dom (f,s)) by XBOOLE_1:16 ; A /\ (great_eq_dom (f,r)) in S by A1, A2, Th13; hence (A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S by A3, A4, FINSUB_1:def_2; ::_thesis: verum end; theorem Th70: :: MESFUNC6:70 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f | A is_simple_func_in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f | A is_simple_func_in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_simple_func_in S holds f | A is_simple_func_in S let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_simple_func_in S holds f | A is_simple_func_in S let A be Element of S; ::_thesis: ( f is_simple_func_in S implies f | A is_simple_func_in S ) assume f is_simple_func_in S ; ::_thesis: f | A is_simple_func_in S then consider F being Finite_Sep_Sequence of S such that A1: dom f = union (rng F) and A2: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y by Def2; deffunc H1( Nat) -> Element of bool X = (F . \$1) /\ A; consider G being FinSequence such that A3: ( len G = len F & ( for n being Nat st n in dom G holds G . n = H1(n) ) ) from FINSEQ_1:sch_2(); A4: rng G c= S proof let P be set ; :: according to TARSKI:def_3 ::_thesis: ( not P in rng G or P in S ) assume P in rng G ; ::_thesis: P in S then consider k being set such that A5: k in dom G and A6: P = G . k by FUNCT_1:def_3; reconsider k = k as Element of NAT by A5; k in Seg (len F) by A3, A5, FINSEQ_1:def_3; then k in dom F by FINSEQ_1:def_3; then A7: F . k in rng F by FUNCT_1:3; G . k = (F . k) /\ A by A3, A5; hence P in S by A6, A7, FINSUB_1:def_2; ::_thesis: verum end; A8: dom G = Seg (len F) by A3, FINSEQ_1:def_3; reconsider G = G as FinSequence of S by A4, FINSEQ_1:def_4; for i, j being Nat st i in dom G & j in dom G & i <> j holds G . i misses G . j proof let i, j be Nat; ::_thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j ) assume that A9: i in dom G and A10: j in dom G and A11: i <> j ; ::_thesis: G . i misses G . j j in Seg (len F) by A3, A10, FINSEQ_1:def_3; then A12: j in dom F by FINSEQ_1:def_3; i in Seg (len F) by A3, A9, FINSEQ_1:def_3; then i in dom F by FINSEQ_1:def_3; then A13: F . i misses F . j by A11, A12, MESFUNC3:4; ( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A3, A9, A10; then (G . i) /\ (G . j) = (((F . i) /\ A) /\ (F . j)) /\ A by XBOOLE_1:16 .= (((F . i) /\ (F . j)) /\ A) /\ A by XBOOLE_1:16 .= ({} /\ A) /\ A by A13, XBOOLE_0:def_7 ; hence G . i misses G . j by XBOOLE_0:def_7; ::_thesis: verum end; then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4; for v being set st v in union (rng G) holds v in dom (f | A) proof let v be set ; ::_thesis: ( v in union (rng G) implies v in dom (f | A) ) assume v in union (rng G) ; ::_thesis: v in dom (f | A) then consider W being set such that A14: v in W and A15: W in rng G by TARSKI:def_4; consider k being set such that A16: k in dom G and A17: W = G . k by A15, FUNCT_1:def_3; reconsider k = k as Element of NAT by A16; k in Seg (len F) by A3, A16, FINSEQ_1:def_3; then k in dom F by FINSEQ_1:def_3; then A18: F . k in rng F by FUNCT_1:3; A19: G . k = (F . k) /\ A by A3, A16; then v in F . k by A14, A17, XBOOLE_0:def_4; then A20: v in union (rng F) by A18, TARSKI:def_4; v in A by A14, A17, A19, XBOOLE_0:def_4; then v in (dom f) /\ A by A1, A20, XBOOLE_0:def_4; hence v in dom (f | A) by RELAT_1:61; ::_thesis: verum end; then A21: union (rng G) c= dom (f | A) by TARSKI:def_3; for v being set st v in dom (f | A) holds v in union (rng G) proof let v be set ; ::_thesis: ( v in dom (f | A) implies v in union (rng G) ) assume v in dom (f | A) ; ::_thesis: v in union (rng G) then A22: v in (dom f) /\ A by RELAT_1:61; then A23: v in A by XBOOLE_0:def_4; v in dom f by A22, XBOOLE_0:def_4; then consider W being set such that A24: v in W and A25: W in rng F by A1, TARSKI:def_4; consider k being set such that A26: k in dom F and A27: W = F . k by A25, FUNCT_1:def_3; reconsider k = k as Element of NAT by A26; A28: k in Seg (len F) by A26, FINSEQ_1:def_3; then k in dom G by A3, FINSEQ_1:def_3; then A29: G . k in rng G by FUNCT_1:3; G . k = (F . k) /\ A by A3, A8, A28; then v in G . k by A23, A24, A27, XBOOLE_0:def_4; hence v in union (rng G) by A29, TARSKI:def_4; ::_thesis: verum end; then dom (f | A) c= union (rng G) by TARSKI:def_3; then A30: dom (f | A) = union (rng G) by A21, XBOOLE_0:def_10; for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds (f | A) . x = (f | A) . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds (f | A) . x = (f | A) . y let x, y be Element of X; ::_thesis: ( n in dom G & x in G . n & y in G . n implies (f | A) . x = (f | A) . y ) assume that A31: n in dom G and A32: x in G . n and A33: y in G . n ; ::_thesis: (f | A) . x = (f | A) . y n in Seg (len F) by A3, A31, FINSEQ_1:def_3; then A34: n in dom F by FINSEQ_1:def_3; G . n = (F . n) /\ A by A3, A31; then ( x in F . n & y in F . n ) by A32, A33, XBOOLE_0:def_4; then A35: f . x = f . y by A2, A34; A36: G . n in rng G by A31, FUNCT_1:3; then x in dom (f | A) by A30, A32, TARSKI:def_4; then A37: (f | A) . x = f . y by A35, FUNCT_1:47; y in dom (f | A) by A30, A33, A36, TARSKI:def_4; hence (f | A) . x = (f | A) . y by A37, FUNCT_1:47; ::_thesis: verum end; hence f | A is_simple_func_in S by A30, Def2; ::_thesis: verum end; theorem Th71: :: MESFUNC6:71 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds dom f is Element of S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL st f is_simple_func_in S holds dom f is Element of S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S holds dom f is Element of S let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S implies dom f is Element of S ) assume f is_simple_func_in S ; ::_thesis: dom f is Element of S then ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) by Def2; hence dom f is Element of S by MESFUNC2:31; ::_thesis: verum end; Lm1: 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,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds ( f + g is_simple_func_in S & dom (f + g) <> {} ) 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,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds ( f + g is_simple_func_in S & dom (f + g) <> {} ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds ( f + g is_simple_func_in S & dom (f + g) <> {} ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f holds ( f + g is_simple_func_in S & dom (f + g) <> {} ) let f, g be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & dom f <> {} & g is_simple_func_in S & dom g = dom f implies ( f + g is_simple_func_in S & dom (f + g) <> {} ) ) assume that A1: f is_simple_func_in S and A2: dom f <> {} and A3: g is_simple_func_in S and A4: dom g = dom f ; ::_thesis: ( f + g is_simple_func_in S & dom (f + g) <> {} ) R_EAL f is_simple_func_in S by A1, Th49; then consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that A5: F,a are_Re-presentation_of R_EAL f by MESFUNC3:12; set la = len F; A6: dom f = union (rng F) by A5, MESFUNC3:def_1; R_EAL g is_simple_func_in S by A3, Th49; then consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that A7: G,b are_Re-presentation_of R_EAL g by MESFUNC3:12; set lb = len G; A8: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; deffunc H1( Nat) -> set = (F . (((\$1 -' 1) div (len G)) + 1)) /\ (G . (((\$1 -' 1) mod (len G)) + 1)); consider FG being FinSequence such that A9: len FG = (len F) * (len G) and A10: for k being Nat st k in dom FG holds FG . k = H1(k) from FINSEQ_1:sch_2(); A11: dom FG = Seg ((len F) * (len G)) by A9, FINSEQ_1:def_3; now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_ FG_._k_in_S reconsider la9 = len F, lb9 = len G as Nat ; let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S ) set i = ((k -' 1) div (len G)) + 1; set j = ((k -' 1) mod (len G)) + 1; assume A12: k in dom FG ; ::_thesis: FG . k in S then A13: k in Seg ((len F) * (len G)) by A9, FINSEQ_1:def_3; then A14: k <= (len F) * (len G) by FINSEQ_1:1; then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; then A15: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24; 1 <= k by A13, FINSEQ_1:1; then A16: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A14, NAT_D:def_3, XXREAL_0:2; A17: len G <> 0 by A13, A14, FINSEQ_1:1; then len G >= 0 + 1 by NAT_1:13; then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A16, NAT_2:15; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A15, XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A17, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len G)) + 1 in Seg (len F) ; then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; then A18: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3; (k -' 1) mod (len G) < len G by A17, NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13; then ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25; then G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3; then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A18, MEASURE1:34; hence FG . k in S by A10, A12; ::_thesis: verum end; then reconsider FG = FG as FinSequence of S by FINSEQ_2:12; for k, l being Nat st k in dom FG & l in dom FG & k <> l holds FG . k misses FG . l proof reconsider la9 = len F, lb9 = len G as Nat ; let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l ) assume that A19: k in dom FG and A20: l in dom FG and A21: k <> l ; ::_thesis: FG . k misses FG . l set j = ((k -' 1) mod (len G)) + 1; set i = ((k -' 1) div (len G)) + 1; A22: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A19; set m = ((l -' 1) mod (len G)) + 1; set n = ((l -' 1) div (len G)) + 1; A23: k in Seg ((len F) * (len G)) by A9, A19, FINSEQ_1:def_3; then A24: 1 <= k by FINSEQ_1:1; then A25: len G <> 0 by A23, FINSEQ_1:1; then (k -' 1) mod (len G) < len G by NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13; then A26: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25; A27: k <= (len F) * (len G) by A23, FINSEQ_1:1; then A28: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A24, NAT_D:def_3, XXREAL_0:2; len G >= 0 + 1 by A25, NAT_1:13; then A29: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A28, NAT_2:15; A30: l in Seg ((len F) * (len G)) by A9, A20, FINSEQ_1:def_3; then A31: 1 <= l by FINSEQ_1:1; A32: now__::_thesis:_(_((k_-'_1)_div_(len_G))_+_1_=_((l_-'_1)_div_(len_G))_+_1_implies_not_((k_-'_1)_mod_(len_G))_+_1_=_((l_-'_1)_mod_(len_G))_+_1_) (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2; then A33: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A31, XREAL_1:233; (k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A25, NAT_D:2; then A34: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A24, XREAL_1:233; assume ( ((k -' 1) div (len G)) + 1 = ((l -' 1) div (len G)) + 1 & ((k -' 1) mod (len G)) + 1 = ((l -' 1) mod (len G)) + 1 ) ; ::_thesis: contradiction hence contradiction by A21, A34, A33; ::_thesis: verum end; k -' 1 <= ((len F) * (len G)) -' 1 by A27, NAT_D:42; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len G)) + 1 in Seg (len F) ; then A35: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; (l -' 1) mod (len G) < len G by A25, NAT_D:1; then ( ((l -' 1) mod (len G)) + 1 >= 0 + 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13; then A36: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25; l <= (len F) * (len G) by A30, FINSEQ_1:1; then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A29, NAT_2:24; then ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((l -' 1) div (len G)) + 1 >= 0 + 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A25, NAT_D:18, XREAL_1:6; then ((l -' 1) div (len G)) + 1 in Seg (len F) ; then A37: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; percases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A32; supposeA38: ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 ; ::_thesis: FG . k misses FG . l (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22; then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16; then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16; then A39: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16; F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A35, A37, A38, MESFUNC3:4; then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A39, XBOOLE_0:def_7; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; supposeA40: ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ; ::_thesis: FG . k misses FG . l (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A10, A20, A22; then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16; then (FG . k) /\ (FG . l) = (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16; then A41: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16; G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A26, A36, A40, MESFUNC3:4; then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A41, XBOOLE_0:def_7; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; end; end; then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4; A42: dom g = union (rng G) by A7, MESFUNC3:def_1; A43: dom f = union (rng FG) proof now__::_thesis:_for_z_being_set_st_z_in_dom_f_holds_ z_in_union_(rng_FG) let z be set ; ::_thesis: ( z in dom f implies z in union (rng FG) ) assume A44: z in dom f ; ::_thesis: z in union (rng FG) then consider Y being set such that A45: z in Y and A46: Y in rng F by A6, TARSKI:def_4; consider i being Nat such that A47: i in dom F and A48: Y = F . i by A46, FINSEQ_2:10; A49: i in Seg (len F) by A47, FINSEQ_1:def_3; then 1 <= i by FINSEQ_1:1; then consider i9 being Nat such that A50: i = 1 + i9 by NAT_1:10; consider Z being set such that A51: z in Z and A52: Z in rng G by A4, A42, A44, TARSKI:def_4; consider j being Nat such that A53: j in dom G and A54: Z = G . j by A52, FINSEQ_2:10; A55: j in Seg (len G) by A53, FINSEQ_1:def_3; then A56: 1 <= j by FINSEQ_1:1; then consider j9 being Nat such that A57: j = 1 + j9 by NAT_1:10; A58: j <= len G by A55, FINSEQ_1:1; then A59: j9 < len G by A57, NAT_1:13; reconsider k = ((i - 1) * (len G)) + j as Nat by A50; A60: k >= 0 + j by A50, XREAL_1:6; then A61: k -' 1 = k - 1 by A56, XREAL_1:233, XXREAL_0:2 .= (i9 * (len G)) + j9 by A50, A57 ; then A62: i = ((k -' 1) div (len G)) + 1 by A50, A59, NAT_D:def_1; i <= len F by A49, FINSEQ_1:1; then i - 1 <= (len F) - 1 by XREAL_1:9; then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64; then A63: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6; (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by A58, XREAL_1:6; then A64: k <= (len F) * (len G) by A63, XXREAL_0:2; k >= 1 by A56, A60, XXREAL_0:2; then A65: k in Seg ((len F) * (len G)) by A64, FINSEQ_1:1; then k in dom FG by A9, FINSEQ_1:def_3; then A66: FG . k in rng FG by FUNCT_1:def_3; A67: j = ((k -' 1) mod (len G)) + 1 by A57, A61, A59, NAT_D:def_2; z in (F . i) /\ (G . j) by A45, A48, A51, A54, XBOOLE_0:def_4; then z in FG . k by A10, A11, A62, A67, A65; hence z in union (rng FG) by A66, TARSKI:def_4; ::_thesis: verum end; hence dom f c= union (rng FG) by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f reconsider la9 = len F, lb9 = len G as Nat ; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f ) assume z in union (rng FG) ; ::_thesis: z in dom f then consider Y being set such that A68: z in Y and A69: Y in rng FG by TARSKI:def_4; consider k being Nat such that A70: k in dom FG and A71: Y = FG . k by A69, FINSEQ_2:10; set j = ((k -' 1) mod (len G)) + 1; set i = ((k -' 1) div (len G)) + 1; A72: k in Seg (len FG) by A70, FINSEQ_1:def_3; then A73: k <= (len F) * (len G) by A9, FINSEQ_1:1; then A74: len G <> 0 by A72, FINSEQ_1:1; then A75: len G >= 0 + 1 by NAT_1:13; 1 <= k by A72, FINSEQ_1:1; then ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A73, NAT_D:def_3, XXREAL_0:2; then A76: ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A75, NAT_2:15; k -' 1 <= ((len F) * (len G)) -' 1 by A73, NAT_D:42; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A76, NAT_2:24; then A77: ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((len F) * (len G)) div (len G) = len F ) by A74, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len G)) + 1 in Seg (len F) by A77; then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; then A78: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def_3; FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A70; then z in F . (((k -' 1) div (len G)) + 1) by A68, A71, XBOOLE_0:def_4; hence z in dom f by A6, A78, TARSKI:def_4; ::_thesis: verum end; for k being Nat for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds (f + g) . x = (f + g) . y proof reconsider la9 = len F, lb9 = len G as Nat ; let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds (f + g) . x = (f + g) . y let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y ) assume that A79: k in dom FG and A80: x in FG . k and A81: y in FG . k ; ::_thesis: (f + g) . x = (f + g) . y set i = ((k -' 1) div (len G)) + 1; set j = ((k -' 1) mod (len G)) + 1; A82: k in Seg (len FG) by A79, FINSEQ_1:def_3; then A83: k <= (len F) * (len G) by A9, FINSEQ_1:1; then A84: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; A85: len G <> 0 by A82, A83, FINSEQ_1:1; then (k -' 1) mod (len G) < len G by NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 0 + 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13; then ((k -' 1) mod (len G)) + 1 in Seg (len G) ; then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3; 1 <= k by A82, FINSEQ_1:1; then A87: ( lb9 divides la9 * lb9 & 1 <= (len F) * (len G) ) by A83, NAT_D:def_3, XXREAL_0:2; len G >= 0 + 1 by A85, NAT_1:13; then ((la9 * lb9) -' 1) div lb9 = ((la9 * lb9) div lb9) - 1 by A87, NAT_2:15; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A84, NAT_2:24; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 0 + 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_D:18, XREAL_1:6; then ((k -' 1) div (len G)) + 1 in Seg (len F) ; then A88: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; A89: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A10, A79; then x in G . (((k -' 1) mod (len G)) + 1) by A80, XBOOLE_0:def_4; then A90: g . x = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def_1; y in G . (((k -' 1) mod (len G)) + 1) by A81, A89, XBOOLE_0:def_4; then A91: g . y = b . (((k -' 1) mod (len G)) + 1) by A7, A86, MESFUNC3:def_1; x in F . (((k -' 1) div (len G)) + 1) by A80, A89, XBOOLE_0:def_4; then f . x = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def_1; then A92: (f . x) + (g . x) = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A90, SUPINF_2:1; y in F . (((k -' 1) div (len G)) + 1) by A81, A89, XBOOLE_0:def_4; then A93: f . y = a . (((k -' 1) div (len G)) + 1) by A5, A88, MESFUNC3:def_1; A94: FG . k in rng FG by A79, FUNCT_1:def_3; then x in dom (f + g) by A4, A43, A8, A80, TARSKI:def_4; then (f + g) . x = (a . (((k -' 1) div (len G)) + 1)) + (b . (((k -' 1) mod (len G)) + 1)) by A92, VALUED_1:def_1; then A95: (f + g) . x = (f . y) + (g . y) by A93, A91, SUPINF_2:1; y in dom (f + g) by A4, A43, A8, A81, A94, TARSKI:def_4; hence (f + g) . x = (f + g) . y by A95, VALUED_1:def_1; ::_thesis: verum end; hence f + g is_simple_func_in S by A4, A43, A8, Def2; ::_thesis: dom (f + g) <> {} thus dom (f + g) <> {} by A2, A4, A8; ::_thesis: verum end; theorem :: MESFUNC6:72 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds f + g is_simple_func_in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds f + g is_simple_func_in S let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL st f is_simple_func_in S & g is_simple_func_in S holds f + g is_simple_func_in S let f, g be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & g is_simple_func_in S implies f + g is_simple_func_in S ) assume A1: ( f is_simple_func_in S & g is_simple_func_in S ) ; ::_thesis: f + g is_simple_func_in S percases ( dom (f + g) = {} or dom (f + g) <> {} ) ; supposeA2: dom (f + g) = {} ; ::_thesis: f + g is_simple_func_in S ex F being Finite_Sep_Sequence of S st ( dom (f + g) = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (f + g) . x = (f + g) . y ) ) proof reconsider EMPTY = {} as Element of S by PROB_1:4; set F = <*EMPTY*>; A3: dom <*EMPTY*> = Seg 1 by FINSEQ_1:38; A4: now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_<*EMPTY*>_&_j_in_dom_<*EMPTY*>_&_i_<>_j_holds_ <*EMPTY*>_._i_misses_<*EMPTY*>_._j let i, j be Nat; ::_thesis: ( i in dom <*EMPTY*> & j in dom <*EMPTY*> & i <> j implies <*EMPTY*> . i misses <*EMPTY*> . j ) assume that A5: i in dom <*EMPTY*> and A6: ( j in dom <*EMPTY*> & i <> j ) ; ::_thesis: <*EMPTY*> . i misses <*EMPTY*> . j i = 1 by A3, A5, FINSEQ_1:2, TARSKI:def_1; hence <*EMPTY*> . i misses <*EMPTY*> . j by A3, A6, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; A7: for n being Nat st n in dom <*EMPTY*> holds <*EMPTY*> . n = EMPTY proof let n be Nat; ::_thesis: ( n in dom <*EMPTY*> implies <*EMPTY*> . n = EMPTY ) assume n in dom <*EMPTY*> ; ::_thesis: <*EMPTY*> . n = EMPTY then n = 1 by A3, FINSEQ_1:2, TARSKI:def_1; hence <*EMPTY*> . n = EMPTY by FINSEQ_1:40; ::_thesis: verum end; reconsider F = <*EMPTY*> as Finite_Sep_Sequence of S by A4, MESFUNC3:4; take F ; ::_thesis: ( dom (f + g) = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (f + g) . x = (f + g) . y ) ) union (rng F) = union (bool {}) by FINSEQ_1:39, ZFMISC_1:1; hence dom (f + g) = union (rng F) by A2; ::_thesis: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (f + g) . x = (f + g) . y thus for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (f + g) . x = (f + g) . y by A7; ::_thesis: verum end; hence f + g is_simple_func_in S by Def2; ::_thesis: verum end; supposeA8: dom (f + g) <> {} ; ::_thesis: f + g is_simple_func_in S A9: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; ( dom f is Element of S & dom g is Element of S ) by A1, Th71; then dom (f + g) in S by A9, FINSUB_1:def_2; then A10: ( f | (dom (f + g)) is_simple_func_in S & g | (dom (f + g)) is_simple_func_in S ) by A1, Th70; dom (f | (dom (f + g))) = (dom f) /\ (dom (f + g)) by RELAT_1:61; then A11: dom (f | (dom (f + g))) = ((dom f) /\ (dom f)) /\ (dom g) by A9, XBOOLE_1:16; dom (g | (dom (f + g))) = (dom g) /\ (dom (f + g)) by RELAT_1:61; then A12: dom (g | (dom (f + g))) = ((dom g) /\ (dom g)) /\ (dom f) by A9, XBOOLE_1:16; then A13: dom (g | (dom (f + g))) = dom (f + g) by VALUED_1:def_1; A14: dom ((f | (dom (f + g))) + (g | (dom (f + g)))) = (dom (f | (dom (f + g)))) /\ (dom (g | (dom (f + g)))) by VALUED_1:def_1 .= dom (f + g) by A11, A12, VALUED_1:def_1 ; A15: for x being Element of X st x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) holds ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x proof let x be Element of X; ::_thesis: ( x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) implies ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x ) assume A16: x in dom ((f | (dom (f + g))) + (g | (dom (f + g)))) ; ::_thesis: ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x then ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = ((f | (dom (f + g))) . x) + ((g | (dom (f + g))) . x) by VALUED_1:def_1 .= (f . x) + ((g | (dom (f + g))) . x) by A14, A16, FUNCT_1:49 .= (f . x) + (g . x) by A14, A16, FUNCT_1:49 ; hence ((f | (dom (f + g))) + (g | (dom (f + g)))) . x = (f + g) . x by A14, A16, VALUED_1:def_1; ::_thesis: verum end; dom (f | (dom (f + g))) = dom (f + g) by A11, VALUED_1:def_1; then (f | (dom (f + g))) + (g | (dom (f + g))) is_simple_func_in S by A8, A10, A13, Lm1; hence f + g is_simple_func_in S by A14, A15, PARTFUN1:5; ::_thesis: verum end; end; end; theorem :: MESFUNC6:73 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for r being Real st f is_simple_func_in S holds r (#) f is_simple_func_in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for r being Real st f is_simple_func_in S holds r (#) f is_simple_func_in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for r being Real st f is_simple_func_in S holds r (#) f is_simple_func_in S let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is_simple_func_in S holds r (#) f is_simple_func_in S let r be Real; ::_thesis: ( f is_simple_func_in S implies r (#) f is_simple_func_in S ) set g = r (#) f; assume f is_simple_func_in S ; ::_thesis: r (#) f is_simple_func_in S then consider G being Finite_Sep_Sequence of S such that A1: dom f = union (rng G) and A2: for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds f . x = f . y by Def2; A3: dom (r (#) f) = dom f by VALUED_1:def_5; now__::_thesis:_for_n_being_Nat for_x,_y_being_Element_of_X_st_n_in_dom_G_&_x_in_G_._n_&_y_in_G_._n_holds_ (r_(#)_f)_._x_=_(r_(#)_f)_._y let n be Nat; ::_thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds (r (#) f) . x = (r (#) f) . y let x, y be Element of X; ::_thesis: ( n in dom G & x in G . n & y in G . n implies (r (#) f) . x = (r (#) f) . y ) assume that A4: n in dom G and A5: x in G . n and A6: y in G . n ; ::_thesis: (r (#) f) . x = (r (#) f) . y A7: G . n in rng G by A4, FUNCT_1:3; then y in dom (r (#) f) by A3, A1, A6, TARSKI:def_4; then A8: (r (#) f) . y = r * (f . y) by VALUED_1:def_5; x in dom (r (#) f) by A3, A1, A5, A7, TARSKI:def_4; then (r (#) f) . x = r * (f . x) by VALUED_1:def_5; hence (r (#) f) . x = (r (#) f) . y by A2, A4, A5, A6, A8; ::_thesis: verum end; hence r (#) f is_simple_func_in S by A3, A1, Def2; ::_thesis: verum end; theorem :: MESFUNC6:74 for X being non empty set for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds g . x <= f . x ) holds f - g is nonnegative proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds g . x <= f . x ) holds f - g is nonnegative let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom (f - g) holds g . x <= f . x ) implies f - g is nonnegative ) A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12; assume for x being set st x in dom (f - g) holds g . x <= f . x ; ::_thesis: f - g is nonnegative hence f - g is nonnegative by A1, Th58; ::_thesis: verum end; theorem :: MESFUNC6:75 for X being non empty set for S being SigmaField of X for A being Element of S for r being Real ex f being PartFunc of X,REAL st ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for r being Real ex f being PartFunc of X,REAL st ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) let S be SigmaField of X; ::_thesis: for A being Element of S for r being Real ex f being PartFunc of X,REAL st ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) let A be Element of S; ::_thesis: for r being Real ex f being PartFunc of X,REAL st ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) let r be Real; ::_thesis: ex f being PartFunc of X,REAL st ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) defpred S1[ set ] means \$1 in A; deffunc H1( set ) -> Real = r; A1: for x being set st S1[x] holds H1(x) in REAL ; consider f being PartFunc of X,REAL such that A2: ( ( for x being set holds ( x in dom f iff ( x in X & S1[x] ) ) ) & ( for x being set st x in dom f holds f . x = H1(x) ) ) from PARTFUN1:sch_3(A1); take f ; ::_thesis: ( f is_simple_func_in S & dom f = A & ( for x being set st x in A holds f . x = r ) ) A3: A c= dom f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in dom f ) assume x in A ; ::_thesis: x in dom f hence x in dom f by A2; ::_thesis: verum end; A4: dom f c= A proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in A ) assume x in dom f ; ::_thesis: x in A hence x in A by A2; ::_thesis: verum end; ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) proof set F = <*(dom f)*>; A5: rng <*(dom f)*> = {(dom f)} by FINSEQ_1:38; then rng <*(dom f)*> = {A} by A4, A3, XBOOLE_0:def_10; then reconsider F = <*(dom f)*> as FinSequence of S by FINSEQ_1:def_4; now__::_thesis:_for_i,_j_being_Nat_st_i_in_dom_F_&_j_in_dom_F_&_i_<>_j_holds_ F_._i_misses_F_._j let i, j be Nat; ::_thesis: ( i in dom F & j in dom F & i <> j implies F . i misses F . j ) assume that A6: i in dom F and A7: ( j in dom F & i <> j ) ; ::_thesis: F . i misses F . j A8: dom F = Seg 1 by FINSEQ_1:38; then i = 1 by A6, FINSEQ_1:2, TARSKI:def_1; hence F . i misses F . j by A7, A8, FINSEQ_1:2, TARSKI:def_1; ::_thesis: verum end; then reconsider F = F as Finite_Sep_Sequence of S by MESFUNC3:4; take F ; ::_thesis: ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) thus dom f = union (rng F) by A5, ZFMISC_1:25; ::_thesis: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y hereby ::_thesis: verum let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y ) assume that A9: n in dom F and A10: x in F . n and A11: y in F . n ; ::_thesis: f . x = f . y dom F = Seg 1 by FINSEQ_1:38; then A12: n = 1 by A9, FINSEQ_1:2, TARSKI:def_1; then x in dom f by A10, FINSEQ_1:40; then A13: f . x = r by A2; y in dom f by A11, A12, FINSEQ_1:40; hence f . x = f . y by A2, A13; ::_thesis: verum end; end; hence f is_simple_func_in S by Def2; ::_thesis: ( dom f = A & ( for x being set st x in A holds f . x = r ) ) thus dom f = A by A4, A3, XBOOLE_0:def_10; ::_thesis: for x being set st x in A holds f . x = r thus for x being set st x in A holds f . x = r by A2; ::_thesis: verum end; theorem :: MESFUNC6:76 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds f | B is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds f | B is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds f | B is_measurable_on A let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds f | B is_measurable_on A let B, A be Element of S; ::_thesis: ( f is_measurable_on B & A = (dom f) /\ B implies f | B is_measurable_on A ) assume that A1: f is_measurable_on B and A2: A = (dom f) /\ B ; ::_thesis: f | B is_measurable_on A A3: R_EAL f is_measurable_on B by A1, Def1; now__::_thesis:_for_r_being_real_number_holds_A_/\_(less_dom_((f_|_B),r))_in_S let r be real number ; ::_thesis: A /\ (less_dom ((f | B),r)) in S now__::_thesis:_for_x_being_set_holds_ (_x_in_A_/\_(less_dom_((f_|_B),r))_iff_x_in_B_/\_(less_dom_(f,r))_) let x be set ; ::_thesis: ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) ) ( x in dom (f | B) & (f | B) . x < R_EAL r iff ( x in (dom f) /\ B & (f | B) . x < R_EAL r ) ) by RELAT_1:61; then A4: ( x in A & x in less_dom ((f | B),r) iff ( x in B & x in dom f & (f | B) . x < R_EAL r ) ) by A2, MESFUNC1:def_11, XBOOLE_0:def_4; ( x in B & x in dom f implies ( f . x < R_EAL r iff (f | B) . x < R_EAL r ) ) by FUNCT_1:49; then ( x in A /\ (less_dom ((f | B),r)) iff ( x in B & x in less_dom (f,r) ) ) by A4, MESFUNC1:def_11, XBOOLE_0:def_4; hence ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) ) by XBOOLE_0:def_4; ::_thesis: verum end; then ( A /\ (less_dom ((f | B),r)) c= B /\ (less_dom (f,r)) & B /\ (less_dom (f,r)) c= A /\ (less_dom ((f | B),r)) ) by TARSKI:def_3; then A /\ (less_dom ((f | B),r)) = B /\ (less_dom (f,r)) by XBOOLE_0:def_10; then A /\ (less_dom ((f | B),(R_EAL r))) in S by A3, MESFUNC1:def_16; hence A /\ (less_dom ((f | B),r)) in S ; ::_thesis: verum end; hence f | B is_measurable_on A by Th12; ::_thesis: verum end; theorem :: MESFUNC6:77 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds (max+ (f + g)) + (max- f) is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds (max+ (f + g)) + (max- f) is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds (max+ (f + g)) + (max- f) is_measurable_on A let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= dom f & f is_measurable_on A & g is_measurable_on A holds (max+ (f + g)) + (max- f) is_measurable_on A let A be Element of S; ::_thesis: ( A c= dom f & f is_measurable_on A & g is_measurable_on A implies (max+ (f + g)) + (max- f) is_measurable_on A ) assume that A1: A c= dom f and A2: f is_measurable_on A and A3: g is_measurable_on A ; ::_thesis: (max+ (f + g)) + (max- f) is_measurable_on A f + g is_measurable_on A by A2, A3, Th26; then A4: max+ (f + g) is_measurable_on A by Th46; max- f is_measurable_on A by A1, A2, Th47; hence (max+ (f + g)) + (max- f) is_measurable_on A by A4, Th26; ::_thesis: verum end; theorem :: MESFUNC6:78 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds (max- (f + g)) + (max+ f) is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds (max- (f + g)) + (max+ f) is_measurable_on A let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds (max- (f + g)) + (max+ f) is_measurable_on A let f, g be PartFunc of X,REAL; ::_thesis: for A being Element of S st A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A holds (max- (f + g)) + (max+ f) is_measurable_on A let A be Element of S; ::_thesis: ( A c= (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A implies (max- (f + g)) + (max+ f) is_measurable_on A ) assume that A1: A c= (dom f) /\ (dom g) and A2: f is_measurable_on A and A3: g is_measurable_on A ; ::_thesis: (max- (f + g)) + (max+ f) is_measurable_on A A4: max+ f is_measurable_on A by A2, Th46; A5: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; f + g is_measurable_on A by A2, A3, Th26; then max- (f + g) is_measurable_on A by A1, A5, Th47; hence (max- (f + g)) + (max+ f) is_measurable_on A by A4, Th26; ::_thesis: verum end; theorem :: MESFUNC6:79 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds dom (f + g) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds dom (f + g) in S let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,REAL st dom f in S & dom g in S holds dom (f + g) in S let f, g be PartFunc of X,REAL; ::_thesis: ( dom f in S & dom g in S implies dom (f + g) in S ) assume ( dom f in S & dom g in S ) ; ::_thesis: dom (f + g) in S then reconsider E1 = dom f, E2 = dom g as Element of S ; dom (f + g) = E1 /\ E2 by VALUED_1:def_1; hence dom (f + g) in S ; ::_thesis: verum end; theorem Th80: :: MESFUNC6:80 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for A, B being Element of S st dom f = A holds ( f is_measurable_on B iff f is_measurable_on A /\ B ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL for A, B being Element of S st dom f = A holds ( f is_measurable_on B iff f is_measurable_on A /\ B ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL for A, B being Element of S st dom f = A holds ( f is_measurable_on B iff f is_measurable_on A /\ B ) let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st dom f = A holds ( f is_measurable_on B iff f is_measurable_on A /\ B ) let A, B be Element of S; ::_thesis: ( dom f = A implies ( f is_measurable_on B iff f is_measurable_on A /\ B ) ) assume A1: dom f = A ; ::_thesis: ( f is_measurable_on B iff f is_measurable_on A /\ B ) A2: now__::_thesis:_for_r_being_real_number_holds_A_/\_(less_dom_(f,r))_=_less_dom_(f,r) let r be real number ; ::_thesis: A /\ (less_dom (f,r)) = less_dom (f,r) now__::_thesis:_for_x_being_set_holds_ (_x_in_A_/\_(less_dom_(f,r))_iff_x_in_less_dom_(f,r)_) let x be set ; ::_thesis: ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) ) ( x in A /\ (less_dom (f,r)) iff ( x in A & x in less_dom (f,r) ) ) by XBOOLE_0:def_4; hence ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) ) by A1, MESFUNC1:def_11; ::_thesis: verum end; then ( A /\ (less_dom (f,r)) c= less_dom (f,r) & less_dom (f,r) c= A /\ (less_dom (f,r)) ) by TARSKI:def_3; hence A /\ (less_dom (f,r)) = less_dom (f,r) by XBOOLE_0:def_10; ::_thesis: verum end; hereby ::_thesis: ( f is_measurable_on A /\ B implies f is_measurable_on B ) assume A3: f is_measurable_on B ; ::_thesis: f is_measurable_on A /\ B now__::_thesis:_for_r_being_real_number_holds_(A_/\_B)_/\_(less_dom_(f,r))_in_S let r be real number ; ::_thesis: (A /\ B) /\ (less_dom (f,r)) in S (A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16 .= B /\ (less_dom (f,r)) by A2 ; hence (A /\ B) /\ (less_dom (f,r)) in S by A3, Th12; ::_thesis: verum end; hence f is_measurable_on A /\ B by Th12; ::_thesis: verum end; assume A4: f is_measurable_on A /\ B ; ::_thesis: f is_measurable_on B now__::_thesis:_for_r_being_real_number_holds_B_/\_(less_dom_(f,r))_in_S let r be real number ; ::_thesis: B /\ (less_dom (f,r)) in S (A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16 .= B /\ (less_dom (f,r)) by A2 ; hence B /\ (less_dom (f,r)) in S by A4, Th12; ::_thesis: verum end; hence f is_measurable_on B by Th12; ::_thesis: verum end; theorem :: MESFUNC6:81 for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds for c being Real for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds for c being Real for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B let S be SigmaField of X; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st dom f = A holds for c being Real for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st dom f = A implies for c being Real for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B ) assume ex A being Element of S st A = dom f ; ::_thesis: for c being Real for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B then consider A being Element of S such that A1: A = dom f ; let c be Real; ::_thesis: for B being Element of S st f is_measurable_on B holds c (#) f is_measurable_on B let B be Element of S; ::_thesis: ( f is_measurable_on B implies c (#) f is_measurable_on B ) assume f is_measurable_on B ; ::_thesis: c (#) f is_measurable_on B then f is_measurable_on A /\ B by A1, Th80; then A2: c (#) f is_measurable_on A /\ B by A1, Th21, XBOOLE_1:17; dom (c (#) f) = A by A1, VALUED_1:def_5; hence c (#) f is_measurable_on B by A2, Th80; ::_thesis: verum end; begin definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,REAL; func Integral (M,f) -> Element of ExtREAL equals :: MESFUNC6:def 3 Integral (M,(R_EAL f)); coherence Integral (M,(R_EAL f)) is Element of ExtREAL ; end; :: deftheorem defines Integral MESFUNC6:def_3_:_ 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,REAL holds Integral (M,f) = Integral (M,(R_EAL f)); theorem Th82: :: MESFUNC6:82 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds Integral (M,f) = integral+ (M,(R_EAL f)) 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds Integral (M,f) = integral+ (M,(R_EAL f)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds Integral (M,f) = integral+ (M,(R_EAL f)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds Integral (M,f) = integral+ (M,(R_EAL f)) let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative implies Integral (M,f) = integral+ (M,(R_EAL f)) ) assume that A1: ex A being Element of S st ( A = dom f & f is_measurable_on A ) and A2: f is nonnegative ; ::_thesis: Integral (M,f) = integral+ (M,(R_EAL f)) consider A being Element of S such that A3: A = dom f and A4: f is_measurable_on A by A1; R_EAL f is_measurable_on A by A4, Def1; hence Integral (M,f) = integral+ (M,(R_EAL f)) by A2, A3, MESFUNC5:88; ::_thesis: verum end; theorem :: MESFUNC6:83 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,REAL st f is_simple_func_in S & f is nonnegative holds ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) 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,REAL st f is_simple_func_in S & f is nonnegative holds ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_simple_func_in S & f is nonnegative holds ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) let f be PartFunc of X,REAL; ::_thesis: ( f is_simple_func_in S & f is nonnegative implies ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) ) assume that A1: f is_simple_func_in S and A2: f is nonnegative ; ::_thesis: ( Integral (M,f) = integral+ (M,(R_EAL f)) & Integral (M,f) = integral' (M,(R_EAL f)) ) A3: R_EAL f is_simple_func_in S by A1, Th49; then reconsider A = dom (R_EAL f) as Element of S by MESFUNC5:37; R_EAL f is_measurable_on A by A3, MESFUNC2:34; then f is_measurable_on A by Def1; hence Integral (M,f) = integral+ (M,(R_EAL f)) by A2, Th82; ::_thesis: Integral (M,f) = integral' (M,(R_EAL f)) hence Integral (M,f) = integral' (M,(R_EAL f)) by A2, A3, MESFUNC5:77; ::_thesis: verum end; theorem :: MESFUNC6:84 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds 0 <= Integral (M,f) 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds 0 <= Integral (M,f) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds 0 <= Integral (M,f) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative holds 0 <= Integral (M,f) let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is nonnegative implies 0 <= Integral (M,f) ) assume that A1: ex A being Element of S st ( A = dom f & f is_measurable_on A ) and A2: f is nonnegative ; ::_thesis: 0 <= Integral (M,f) consider A being Element of S such that A3: A = dom f and A4: f is_measurable_on A by A1; R_EAL f is_measurable_on A by A4, Def1; hence 0 <= Integral (M,f) by A2, A3, MESFUNC5:90; ::_thesis: verum end; theorem :: MESFUNC6:85 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,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) 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,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let A, B be Element of S; ::_thesis: ( ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: ( f is nonnegative & A misses B ) ; ::_thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) consider E being Element of S such that A3: E = dom f and A4: f is_measurable_on E by A1; R_EAL f is_measurable_on E by A4, Def1; hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A3, MESFUNC5:91; ::_thesis: verum end; theorem :: MESFUNC6:86 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,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative holds 0 <= Integral (M,(f | A)) 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,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative holds 0 <= Integral (M,(f | A)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative holds 0 <= Integral (M,(f | A)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative holds 0 <= Integral (M,(f | A)) let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative holds 0 <= Integral (M,(f | A)) let A be Element of S; ::_thesis: ( ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative implies 0 <= Integral (M,(f | A)) ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: f is nonnegative ; ::_thesis: 0 <= Integral (M,(f | A)) consider E being Element of S such that A3: E = dom f and A4: f is_measurable_on E by A1; R_EAL f is_measurable_on E by A4, Def1; hence 0 <= Integral (M,(f | A)) by A2, A3, MESFUNC5:92; ::_thesis: verum end; theorem :: MESFUNC6:87 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,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds Integral (M,(f | A)) <= Integral (M,(f | B)) 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,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds Integral (M,(f | A)) <= Integral (M,(f | B)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds Integral (M,(f | A)) <= Integral (M,(f | B)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds Integral (M,(f | A)) <= Integral (M,(f | B)) let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B holds Integral (M,(f | A)) <= Integral (M,(f | B)) let A, B be Element of S; ::_thesis: ( ex E being Element of S st ( E = dom f & f is_measurable_on E ) & f is nonnegative & A c= B implies Integral (M,(f | A)) <= Integral (M,(f | B)) ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: ( f is nonnegative & A c= B ) ; ::_thesis: Integral (M,(f | A)) <= Integral (M,(f | B)) consider E being Element of S such that A3: E = dom f and A4: f is_measurable_on E by A1; R_EAL f is_measurable_on E by A4, Def1; hence Integral (M,(f | A)) <= Integral (M,(f | B)) by A2, A3, MESFUNC5:93; ::_thesis: verum end; theorem :: MESFUNC6:88 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,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 holds Integral (M,(f | A)) = 0 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,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 holds Integral (M,(f | A)) = 0 let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 holds Integral (M,(f | A)) = 0 let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 holds Integral (M,(f | A)) = 0 let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 holds Integral (M,(f | A)) = 0 let A be Element of S; ::_thesis: ( ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 implies Integral (M,(f | A)) = 0 ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: M . A = 0 ; ::_thesis: Integral (M,(f | A)) = 0 consider E being Element of S such that A3: E = dom f and A4: f is_measurable_on E by A1; R_EAL f is_measurable_on E by A4, Def1; hence Integral (M,(f | A)) = 0 by A2, A3, MESFUNC5:94; ::_thesis: verum end; theorem :: MESFUNC6:89 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,REAL for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) 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,REAL for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) let f be PartFunc of X,REAL; ::_thesis: for E, A being Element of S st E = dom f & f is_measurable_on E & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) let E, A be Element of S; ::_thesis: ( E = dom f & f is_measurable_on E & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) ) assume that A1: E = dom f and A2: f is_measurable_on E and A3: M . A = 0 ; ::_thesis: Integral (M,(f | (E \ A))) = Integral (M,f) R_EAL f is_measurable_on E by A2, Def1; hence Integral (M,(f | (E \ A))) = Integral (M,f) by A1, A3, MESFUNC5:95; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,REAL; predf is_integrable_on M means :Def4: :: MESFUNC6:def 4 R_EAL f is_integrable_on M; end; :: deftheorem Def4 defines is_integrable_on MESFUNC6:def_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,REAL holds ( f is_integrable_on M iff R_EAL f is_integrable_on M ); theorem :: MESFUNC6:90 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,REAL st f is_integrable_on M holds ( -infty < Integral (M,f) & Integral (M,f) < +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,REAL st f is_integrable_on M holds ( -infty < Integral (M,f) & Integral (M,f) < +infty ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st f is_integrable_on M holds ( -infty < Integral (M,f) & Integral (M,f) < +infty ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_integrable_on M holds ( -infty < Integral (M,f) & Integral (M,f) < +infty ) let f be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M implies ( -infty < Integral (M,f) & Integral (M,f) < +infty ) ) assume f is_integrable_on M ; ::_thesis: ( -infty < Integral (M,f) & Integral (M,f) < +infty ) then R_EAL f is_integrable_on M by Def4; hence ( -infty < Integral (M,f) & Integral (M,f) < +infty ) by MESFUNC5:96; ::_thesis: verum end; theorem :: MESFUNC6:91 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,REAL for A being Element of S st f is_integrable_on M holds f | A is_integrable_on M 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,REAL for A being Element of S st f is_integrable_on M holds f | A is_integrable_on M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A being Element of S st f is_integrable_on M holds f | A is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A being Element of S st f is_integrable_on M holds f | A is_integrable_on M let f be PartFunc of X,REAL; ::_thesis: for A being Element of S st f is_integrable_on M holds f | A is_integrable_on M let A be Element of S; ::_thesis: ( f is_integrable_on M implies f | A is_integrable_on M ) assume f is_integrable_on M ; ::_thesis: f | A is_integrable_on M then R_EAL f is_integrable_on M by Def4; then R_EAL (f | A) is_integrable_on M by MESFUNC5:97; hence f | A is_integrable_on M by Def4; ::_thesis: verum end; theorem :: MESFUNC6:92 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,REAL for A, B being Element of S st f is_integrable_on M & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) 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,REAL for A, B being Element of S st f is_integrable_on M & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for A, B being Element of S st f is_integrable_on M & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for A, B being Element of S st f is_integrable_on M & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let f be PartFunc of X,REAL; ::_thesis: for A, B being Element of S st f is_integrable_on M & A misses B holds Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) let A, B be Element of S; ::_thesis: ( f is_integrable_on M & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) assume that A1: f is_integrable_on M and A2: A misses B ; ::_thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) R_EAL f is_integrable_on M by A1, Def4; hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, MESFUNC5:98; ::_thesis: verum end; theorem :: MESFUNC6:93 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,REAL for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) 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,REAL for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) let f be PartFunc of X,REAL; ::_thesis: for B, A being Element of S st f is_integrable_on M & B = (dom f) \ A holds ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) let B, A be Element of S; ::_thesis: ( f is_integrable_on M & B = (dom f) \ A implies ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) ) assume that A1: f is_integrable_on M and A2: B = (dom f) \ A ; ::_thesis: ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) A3: R_EAL f is_integrable_on M by A1, Def4; then R_EAL (f | A) is_integrable_on M by A2, MESFUNC5:99; hence f | A is_integrable_on M by Def4; ::_thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) thus Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A2, A3, MESFUNC5:99; ::_thesis: verum end; theorem :: MESFUNC6:94 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff abs f is_integrable_on M ) 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff abs f is_integrable_on M ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff abs f is_integrable_on M ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff abs f is_integrable_on M ) let f be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff abs f is_integrable_on M ) ) assume ex A being Element of S st ( A = dom f & f is_measurable_on A ) ; ::_thesis: ( f is_integrable_on M iff abs f is_integrable_on M ) then consider A being Element of S such that A1: A = dom f and A2: f is_measurable_on A ; R_EAL f is_measurable_on A by A2, Def1; then ( R_EAL f is_integrable_on M iff |.(R_EAL f).| is_integrable_on M ) by A1, MESFUNC5:100; then ( f is_integrable_on M iff R_EAL (abs f) is_integrable_on M ) by Def4, Th1; hence ( f is_integrable_on M iff abs f is_integrable_on M ) by Def4; ::_thesis: verum end; theorem :: MESFUNC6:95 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,REAL st f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,(abs f)) 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,REAL st f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,(abs f)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL st f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,(abs f)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL st f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,(abs f)) let f be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M implies |.(Integral (M,f)).| <= Integral (M,(abs f)) ) assume f is_integrable_on M ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,(abs f)) then R_EAL f is_integrable_on M by Def4; then |.(Integral (M,f)).| <= Integral (M,|.(R_EAL f).|) by MESFUNC5:101; hence |.(Integral (M,f)).| <= Integral (M,(abs f)) by Th1; ::_thesis: verum end; theorem :: MESFUNC6:96 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds abs (f . x) <= g . x ) holds ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) 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,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds abs (f . x) <= g . x ) holds ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds abs (f . x) <= g . x ) holds ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds abs (f . x) <= g . x ) holds ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) let f, g be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds abs (f . x) <= g . x ) implies ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) ) assume that A1: ex A being Element of S st ( A = dom f & f is_measurable_on A ) and A2: dom f = dom g and A3: g is_integrable_on M and A4: for x being Element of X st x in dom f holds abs (f . x) <= g . x ; ::_thesis: ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) A5: R_EAL g is_integrable_on M by A3, Def4; A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(R_EAL_f)_holds_ |.((R_EAL_f)_._x).|_<=_(R_EAL_g)_._x let x be Element of X; ::_thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (R_EAL g) . x ) A7: abs (f . x) = |.((R_EAL f) . x).| by EXTREAL2:1; assume x in dom (R_EAL f) ; ::_thesis: |.((R_EAL f) . x).| <= (R_EAL g) . x hence |.((R_EAL f) . x).| <= (R_EAL g) . x by A4, A7; ::_thesis: verum end; consider A being Element of S such that A8: A = dom f and A9: f is_measurable_on A by A1; R_EAL f is_measurable_on A by A9, Def1; then ( R_EAL f is_integrable_on M & Integral (M,|.(R_EAL f).|) <= Integral (M,(R_EAL g)) ) by A2, A8, A5, A6, MESFUNC5:102; hence ( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) ) by Def4, Th1; ::_thesis: verum end; theorem :: MESFUNC6:97 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,REAL for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) holds Integral (M,f) = (R_EAL r) * (M . (dom f)) 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,REAL for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) holds Integral (M,f) = (R_EAL r) * (M . (dom f)) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) holds Integral (M,f) = (R_EAL r) * (M . (dom f)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) holds Integral (M,f) = (R_EAL r) * (M . (dom f)) let f be PartFunc of X,REAL; ::_thesis: for r being Real st dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) holds Integral (M,f) = (R_EAL r) * (M . (dom f)) let r be Real; ::_thesis: ( dom f in S & 0 <= r & ( for x being set st x in dom f holds f . x = r ) implies Integral (M,f) = (R_EAL r) * (M . (dom f)) ) assume that A1: dom f in S and A2: 0 <= r and A3: for x being set st x in dom f holds f . x = r ; ::_thesis: Integral (M,f) = (R_EAL r) * (M . (dom f)) A4: for x being set st x in dom (R_EAL f) holds 0. <= (R_EAL f) . x by A2, A3; reconsider A = dom (R_EAL f) as Element of S by A1; A5: R_EAL f is_measurable_on A by A3, Th2, MESFUNC2:34; ( (R_EAL r) * (M . (dom (R_EAL f))) = integral' (M,(R_EAL f)) & R_EAL f is_simple_func_in S ) by A1, A2, A3, Th2, MESFUNC5:104; then integral+ (M,(R_EAL f)) = (R_EAL r) * (M . (dom (R_EAL f))) by A4, MESFUNC5:77, SUPINF_2:52; hence Integral (M,f) = (R_EAL r) * (M . (dom f)) by A4, A5, MESFUNC5:88, SUPINF_2:52; ::_thesis: verum end; theorem :: MESFUNC6:98 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,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds f + g is_integrable_on M 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,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds f + g is_integrable_on M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds f + g is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative holds f + g is_integrable_on M let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is nonnegative implies f + g is_integrable_on M ) assume that A1: ( f is_integrable_on M & g is_integrable_on M ) and A2: ( f is nonnegative & g is nonnegative ) ; ::_thesis: f + g is_integrable_on M ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by A1, Def4; then (R_EAL f) + (R_EAL g) is_integrable_on M by A2, MESFUNC5:106; then R_EAL (f + g) is_integrable_on M by Th23; hence f + g is_integrable_on M by Def4; ::_thesis: verum end; theorem :: MESFUNC6:99 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,REAL st f is_integrable_on M & g is_integrable_on M holds dom (f + g) in S 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,REAL st f is_integrable_on M & g is_integrable_on M holds dom (f + g) in S let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds dom (f + g) in S let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds dom (f + g) in S let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S ) assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: dom (f + g) in S then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4; then dom ((R_EAL f) + (R_EAL g)) in S by MESFUNC5:107; then dom (R_EAL (f + g)) in S by Th23; hence dom (f + g) in S ; ::_thesis: verum end; theorem :: MESFUNC6:100 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,REAL st f is_integrable_on M & g is_integrable_on M holds f + g is_integrable_on M 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,REAL st f is_integrable_on M & g is_integrable_on M holds f + g is_integrable_on M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds f + g is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds f + g is_integrable_on M let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M ) assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: f + g is_integrable_on M then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4; then (R_EAL f) + (R_EAL g) is_integrable_on M by MESFUNC5:108; then R_EAL (f + g) is_integrable_on M by Th23; hence f + g is_integrable_on M by Def4; ::_thesis: verum end; theorem :: MESFUNC6:101 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,REAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + 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,REAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + 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,REAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) let f, g be PartFunc of X,REAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) ) assume ( f is_integrable_on M & g is_integrable_on M ) ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) then ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by Def4; then consider E being Element of S such that A1: ( E = (dom (R_EAL f)) /\ (dom (R_EAL g)) & Integral (M,((R_EAL f) + (R_EAL g))) = (Integral (M,((R_EAL f) | E))) + (Integral (M,((R_EAL g) | E))) ) by MESFUNC5:109; take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) thus ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A1, Th23; ::_thesis: verum end; theorem :: MESFUNC6:102 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,REAL for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) 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,REAL for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) let r be Real; ::_thesis: ( f is_integrable_on M implies ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) ) assume f is_integrable_on M ; ::_thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) then A1: R_EAL f is_integrable_on M by Def4; then r (#) (R_EAL f) is_integrable_on M by MESFUNC5:110; then A2: R_EAL (r (#) f) is_integrable_on M by Th20; Integral (M,(r (#) (R_EAL f))) = (R_EAL r) * (Integral (M,(R_EAL f))) by A1, MESFUNC5:110; hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = (R_EAL r) * (Integral (M,f)) ) by A2, Def4, Th20; ::_thesis: verum end; definition let X be non empty set ; let S be SigmaField of X; let M be sigma_Measure of S; let f be PartFunc of X,REAL; let B be Element of S; func Integral_on (M,B,f) -> Element of ExtREAL equals :: MESFUNC6:def 5 Integral (M,(f | B)); coherence Integral (M,(f | B)) is Element of ExtREAL ; end; :: deftheorem defines Integral_on MESFUNC6:def_5_:_ 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,REAL for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B)); theorem :: MESFUNC6:103 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,REAL for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) 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,REAL for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) let f, g be PartFunc of X,REAL; ::_thesis: for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) let B be Element of S; ::_thesis: ( f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) implies ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) ) assume that A1: ( f is_integrable_on M & g is_integrable_on M ) and A2: B c= dom (f + g) ; ::_thesis: ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) A3: dom (f + g) = dom (R_EAL (f + g)) .= dom ((R_EAL f) + (R_EAL g)) by Th23 ; A4: ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by A1, Def4; then (R_EAL f) + (R_EAL g) is_integrable_on M by A2, A3, MESFUNC5:111; then A5: R_EAL (f + g) is_integrable_on M by Th23; Integral_on (M,B,((R_EAL f) + (R_EAL g))) = (Integral_on (M,B,(R_EAL f))) + (Integral_on (M,B,(R_EAL g))) by A2, A4, A3, MESFUNC5:111; hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A5, Def4, Th23; ::_thesis: verum end; theorem :: MESFUNC6:104 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,REAL for r being Real for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) 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,REAL for r being Real for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,REAL for r being Real for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for r being Real for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) let f be PartFunc of X,REAL; ::_thesis: for r being Real for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) let r be Real; ::_thesis: for B being Element of S st f is_integrable_on M holds ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) let B be Element of S; ::_thesis: ( f is_integrable_on M implies ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) ) assume f is_integrable_on M ; ::_thesis: ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) then A1: R_EAL f is_integrable_on M by Def4; then Integral_on (M,B,(r (#) (R_EAL f))) = (R_EAL r) * (Integral_on (M,B,(R_EAL f))) by MESFUNC5:112; then A2: Integral_on (M,B,(R_EAL (r (#) f))) = (R_EAL r) * (Integral_on (M,B,(R_EAL f))) by Th20; R_EAL (f | B) is_integrable_on M by A1, MESFUNC5:112; hence ( f | B is_integrable_on M & Integral_on (M,B,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) ) by A2, Def4; ::_thesis: verum end;