:: MESFUN6C semantic presentation begin theorem Th1: :: MESFUN6C:1 for a, b being real number holds ( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b ) proof let a, b be real number ; ::_thesis: ( (R_EAL a) + (R_EAL b) = a + b & - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b ) reconsider a9 = a, b9 = b as Real by XREAL_0:def_1; A1: b9 = R_EAL b ; A2: a9 = R_EAL a ; hence (R_EAL a) + (R_EAL b) = a + b by A1, SUPINF_2:1; ::_thesis: ( - (R_EAL a) = - a & (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b ) - a9 = R_EAL (- a) ; hence - (R_EAL a) = - a by SUPINF_2:2; ::_thesis: ( (R_EAL a) - (R_EAL b) = a - b & (R_EAL a) * (R_EAL b) = a * b ) thus (R_EAL a) - (R_EAL b) = a - b by A2, A1, SUPINF_2:3; ::_thesis: (R_EAL a) * (R_EAL b) = a * b thus (R_EAL a) * (R_EAL b) = a * b by A2, A1, EXTREAL1:1; ::_thesis: verum end; begin definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,COMPLEX; let E be Element of S; predf is_measurable_on E means :Def1: :: MESFUN6C:def 1 ( Re f is_measurable_on E & Im f is_measurable_on E ); end; :: deftheorem Def1 defines is_measurable_on MESFUN6C:def_1_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for E being Element of S holds ( f is_measurable_on E iff ( Re f is_measurable_on E & Im f is_measurable_on E ) ); theorem Th2: :: MESFUN6C:2 for X being non empty set for f being PartFunc of X,COMPLEX for r being Real holds ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX for r being Real holds ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) ) let f be PartFunc of X,COMPLEX; ::_thesis: for r being Real holds ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) ) let r be Real; ::_thesis: ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) ) A1: dom (r (#) (Re f)) = dom (Re f) by VALUED_1:def_5; A2: Im r = 0 by COMPLEX1:def_2; A3: dom (Re f) = dom f by COMSEQ_3:def_3; A4: Re r = r by COMPLEX1:def_1; A5: dom (r (#) f) = dom f by VALUED_1:def_5; A6: dom (Re (r (#) f)) = dom (r (#) f) by COMSEQ_3:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_(Re_f))_holds_ (r_(#)_(Re_f))_._x_=_(Re_(r_(#)_f))_._x let x be set ; ::_thesis: ( x in dom (r (#) (Re f)) implies (r (#) (Re f)) . x = (Re (r (#) f)) . x ) A7: Re (r * (f . x)) = ((Re r) * (Re (f . x))) - ((Im r) * (Im (f . x))) by COMPLEX1:9; assume A8: x in dom (r (#) (Re f)) ; ::_thesis: (r (#) (Re f)) . x = (Re (r (#) f)) . x then A9: (Re f) . x = Re (f . x) by A1, COMSEQ_3:def_3; (Re (r (#) f)) . x = Re ((r (#) f) . x) by A1, A5, A6, A3, A8, COMSEQ_3:def_3; then (Re (r (#) f)) . x = r * (Re (f . x)) by A1, A5, A3, A4, A2, A8, A7, VALUED_1:def_5; hence (r (#) (Re f)) . x = (Re (r (#) f)) . x by A8, A9, VALUED_1:def_5; ::_thesis: verum end; hence r (#) (Re f) = Re (r (#) f) by A1, A5, A6, A3, FUNCT_1:2; ::_thesis: r (#) (Im f) = Im (r (#) f) A10: dom (r (#) (Im f)) = dom (Im f) by VALUED_1:def_5; A11: dom (Im f) = dom f by COMSEQ_3:def_4; A12: dom (Im (r (#) f)) = dom (r (#) f) by COMSEQ_3:def_4; now__::_thesis:_for_x_being_set_st_x_in_dom_(r_(#)_(Im_f))_holds_ (r_(#)_(Im_f))_._x_=_(Im_(r_(#)_f))_._x let x be set ; ::_thesis: ( x in dom (r (#) (Im f)) implies (r (#) (Im f)) . x = (Im (r (#) f)) . x ) A13: Im (r * (f . x)) = ((Im r) * (Re (f . x))) + ((Re r) * (Im (f . x))) by COMPLEX1:9; assume A14: x in dom (r (#) (Im f)) ; ::_thesis: (r (#) (Im f)) . x = (Im (r (#) f)) . x then A15: (Im f) . x = Im (f . x) by A10, COMSEQ_3:def_4; (Im (r (#) f)) . x = Im ((r (#) f) . x) by A10, A5, A12, A11, A14, COMSEQ_3:def_4; then (Im (r (#) f)) . x = r * (Im (f . x)) by A10, A5, A11, A4, A2, A14, A13, VALUED_1:def_5; hence (r (#) (Im f)) . x = (Im (r (#) f)) . x by A14, A15, VALUED_1:def_5; ::_thesis: verum end; hence r (#) (Im f) = Im (r (#) f) by A10, A5, A12, A11, FUNCT_1:2; ::_thesis: verum end; theorem Th3: :: MESFUN6C:3 for X being non empty set for f being PartFunc of X,COMPLEX for c being complex number holds ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX for c being complex number holds ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) ) let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number holds ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) ) let c be complex number ; ::_thesis: ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) ) A1: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5; A2: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5; A3: dom (c (#) f) = dom f by VALUED_1:def_5; A4: dom (Re (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_3; A5: dom (Re f) = dom f by COMSEQ_3:def_3; A6: dom (Im f) = dom f by COMSEQ_3:def_4; A7: dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12; now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(c_(#)_f))_holds_ (Re_(c_(#)_f))_._x_=_(((Re_c)_(#)_(Re_f))_-_((Im_c)_(#)_(Im_f)))_._x let x be set ; ::_thesis: ( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x ) A8: Re (c * (f . x)) = ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x))) by COMPLEX1:9; assume A9: x in dom (Re (c (#) f)) ; ::_thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x then A10: ((Im c) (#) (Im f)) . x = (Im c) * ((Im f) . x) by A4, A6, A2, A3, VALUED_1:def_5; A11: (Im f) . x = Im (f . x) by A4, A6, A3, A9, COMSEQ_3:def_4; A12: (Re f) . x = Re (f . x) by A4, A5, A3, A9, COMSEQ_3:def_3; (Re (c (#) f)) . x = Re ((c (#) f) . x) by A9, COMSEQ_3:def_3; then A13: (Re (c (#) f)) . x = Re (c * (f . x)) by A4, A9, VALUED_1:def_5; ((Re c) (#) (Re f)) . x = (Re c) * ((Re f) . x) by A4, A5, A1, A3, A9, VALUED_1:def_5; hence (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x by A4, A5, A6, A1, A2, A3, A7, A9, A13, A10, A12, A11, A8, VALUED_1:13; ::_thesis: verum end; hence Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) by A4, A5, A6, A1, A2, A3, A7, FUNCT_1:2; ::_thesis: Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) A14: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5; A15: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5; A16: dom (Im (c (#) f)) = dom (c (#) f) by COMSEQ_3:def_4; A17: dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(c_(#)_f))_holds_ (Im_(c_(#)_f))_._x_=_(((Im_c)_(#)_(Re_f))_+_((Re_c)_(#)_(Im_f)))_._x let x be set ; ::_thesis: ( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x ) assume A18: x in dom (Im (c (#) f)) ; ::_thesis: (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x then A19: ((Im c) (#) (Re f)) . x = (Im c) * ((Re f) . x) by A5, A16, A14, A3, VALUED_1:def_5; (Im (c (#) f)) . x = Im ((c (#) f) . x) by A18, COMSEQ_3:def_4; then A20: (Im (c (#) f)) . x = Im (c * (f . x)) by A16, A18, VALUED_1:def_5; A21: (Im f) . x = Im (f . x) by A16, A6, A3, A18, COMSEQ_3:def_4; A22: (Re f) . x = Re (f . x) by A5, A16, A3, A18, COMSEQ_3:def_3; A23: ((Re c) (#) (Im f)) . x = (Re c) * ((Im f) . x) by A16, A6, A15, A3, A18, VALUED_1:def_5; (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x = (((Im c) (#) (Re f)) . x) + (((Re c) (#) (Im f)) . x) by A5, A16, A6, A14, A15, A3, A17, A18, VALUED_1:def_1; hence (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x by A20, A19, A23, A22, A21, COMPLEX1:9; ::_thesis: verum end; hence Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) by A5, A16, A6, A14, A15, A3, A17, FUNCT_1:2; ::_thesis: verum end; theorem Th4: :: MESFUN6C:4 for X being non empty set for f being PartFunc of X,COMPLEX holds ( - (Im f) = Re ( (#) f) & Re f = Im ( (#) f) ) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds ( - (Im f) = Re ( (#) f) & Re f = Im ( (#) f) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( - (Im f) = Re ( (#) f) & Re f = Im ( (#) f) ) A1: dom (- (Im f)) = dom (Im f) by VALUED_1:8; A2: dom ( (#) f) = dom f by VALUED_1:def_5; A3: dom (Im f) = dom f by COMSEQ_3:def_4; A4: dom (Re ( (#) f)) = dom ( (#) f) by COMSEQ_3:def_3; now__::_thesis:_for_x_being_set_st_x_in_dom_(-_(Im_f))_holds_ (-_(Im_f))_._x_=_(Re_(_(#)_f))_._x let x be set ; ::_thesis: ( x in dom (- (Im f)) implies (- (Im f)) . x = (Re ( (#) f)) . x ) A5: (- (Im f)) . x = - ((Im f) . x) by VALUED_1:8; A6: Re ( * (f . x)) = ((Re ) * (Re (f . x))) - ((Im ) * (Im (f . x))) by COMPLEX1:9; assume A7: x in dom (- (Im f)) ; ::_thesis: (- (Im f)) . x = (Re ( (#) f)) . x then (Re ( (#) f)) . x = Re (( (#) f) . x) by A1, A4, A2, A3, COMSEQ_3:def_3; then (Re ( (#) f)) . x = - (Im (f . x)) by A1, A2, A3, A7, A6, COMPLEX1:7, VALUED_1:def_5; hence (- (Im f)) . x = (Re ( (#) f)) . x by A1, A7, A5, COMSEQ_3:def_4; ::_thesis: verum end; hence - (Im f) = Re ( (#) f) by A4, A2, A3, FUNCT_1:2, VALUED_1:8; ::_thesis: Re f = Im ( (#) f) A8: dom (Re f) = dom f by COMSEQ_3:def_3; A9: dom (Im ( (#) f)) = dom ( (#) f) by COMSEQ_3:def_4; now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_f)_holds_ (Re_f)_._x_=_(Im_(_(#)_f))_._x let x be set ; ::_thesis: ( x in dom (Re f) implies (Re f) . x = (Im ( (#) f)) . x ) A10: Im ( * (f . x)) = ((Im ) * (Re (f . x))) + ((Re ) * (Im (f . x))) by COMPLEX1:9; assume A11: x in dom (Re f) ; ::_thesis: (Re f) . x = (Im ( (#) f)) . x then (Im ( (#) f)) . x = Im (( (#) f) . x) by A8, A2, A9, COMSEQ_3:def_4; then (Im ( (#) f)) . x = Re (f . x) by A8, A2, A11, A10, COMPLEX1:7, VALUED_1:def_5; hence (Re f) . x = (Im ( (#) f)) . x by A11, COMSEQ_3:def_3; ::_thesis: verum end; hence Re f = Im ( (#) f) by A8, A2, A9, FUNCT_1:2; ::_thesis: verum end; theorem Th5: :: MESFUN6C:5 for X being non empty set for f, g being PartFunc of X,COMPLEX holds ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) ) A1: dom (Re (f + g)) = dom (f + g) by COMSEQ_3:def_3; A2: dom (Re g) = dom g by COMSEQ_3:def_3; A3: dom (Re f) = dom f by COMSEQ_3:def_3; then dom ((Re f) + (Re g)) = (dom f) /\ (dom g) by A2, VALUED_1:def_1; then A4: dom (Re (f + g)) = dom ((Re f) + (Re g)) by A1, VALUED_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(f_+_g))_holds_ (Re_(f_+_g))_._x_=_((Re_f)_+_(Re_g))_._x let x be set ; ::_thesis: ( x in dom (Re (f + g)) implies (Re (f + g)) . x = ((Re f) + (Re g)) . x ) assume A5: x in dom (Re (f + g)) ; ::_thesis: (Re (f + g)) . x = ((Re f) + (Re g)) . x then (Re (f + g)) . x = Re ((f + g) . x) by COMSEQ_3:def_3; then (Re (f + g)) . x = Re ((f . x) + (g . x)) by A1, A5, VALUED_1:def_1; then A6: (Re (f + g)) . x = (Re (f . x)) + (Re (g . x)) by COMPLEX1:8; A7: x in (dom f) /\ (dom g) by A1, A5, VALUED_1:def_1; then x in dom (Re g) by A2, XBOOLE_0:def_4; then A8: (Re g) . x = Re (g . x) by COMSEQ_3:def_3; x in dom (Re f) by A3, A7, XBOOLE_0:def_4; then (Re f) . x = Re (f . x) by COMSEQ_3:def_3; hence (Re (f + g)) . x = ((Re f) + (Re g)) . x by A4, A5, A6, A8, VALUED_1:def_1; ::_thesis: verum end; hence Re (f + g) = (Re f) + (Re g) by A4, FUNCT_1:2; ::_thesis: Im (f + g) = (Im f) + (Im g) A9: dom (Im (f + g)) = dom (f + g) by COMSEQ_3:def_4; A10: dom (Im g) = dom g by COMSEQ_3:def_4; A11: dom (Im f) = dom f by COMSEQ_3:def_4; then dom ((Im f) + (Im g)) = (dom f) /\ (dom g) by A10, VALUED_1:def_1; then A12: dom (Im (f + g)) = dom ((Im f) + (Im g)) by A9, VALUED_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(f_+_g))_holds_ (Im_(f_+_g))_._x_=_((Im_f)_+_(Im_g))_._x let x be set ; ::_thesis: ( x in dom (Im (f + g)) implies (Im (f + g)) . x = ((Im f) + (Im g)) . x ) assume A13: x in dom (Im (f + g)) ; ::_thesis: (Im (f + g)) . x = ((Im f) + (Im g)) . x then (Im (f + g)) . x = Im ((f + g) . x) by COMSEQ_3:def_4; then (Im (f + g)) . x = Im ((f . x) + (g . x)) by A9, A13, VALUED_1:def_1; then A14: (Im (f + g)) . x = (Im (f . x)) + (Im (g . x)) by COMPLEX1:8; A15: x in (dom f) /\ (dom g) by A9, A13, VALUED_1:def_1; then x in dom (Im g) by A10, XBOOLE_0:def_4; then A16: (Im g) . x = Im (g . x) by COMSEQ_3:def_4; x in dom (Im f) by A11, A15, XBOOLE_0:def_4; then (Im f) . x = Im (f . x) by COMSEQ_3:def_4; hence (Im (f + g)) . x = ((Im f) + (Im g)) . x by A12, A13, A14, A16, VALUED_1:def_1; ::_thesis: verum end; hence Im (f + g) = (Im f) + (Im g) by A12, FUNCT_1:2; ::_thesis: verum end; theorem Th6: :: MESFUN6C:6 for X being non empty set for f, g being PartFunc of X,COMPLEX holds ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) Re (f - g) = (Re f) + (Re (- g)) by Th5; then A1: Re (f - g) = (Re f) + ((- 1) (#) (Re g)) by Th2; Im (f - g) = (Im f) + (Im (- g)) by Th5; hence ( Re (f - g) = (Re f) - (Re g) & Im (f - g) = (Im f) - (Im g) ) by A1, Th2; ::_thesis: verum end; theorem Th7: :: MESFUN6C:7 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for A being Element of S holds ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX for A being Element of S holds ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX for A being Element of S holds ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S holds ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) let A be Element of S; ::_thesis: ( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) ) dom ((Re f) | A) = (dom (Re f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_3 ; then A1: dom ((Re f) | A) = dom (f | A) by RELAT_1:61 .= dom (Re (f | A)) by COMSEQ_3:def_3 ; now__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_|_A)_holds_ (Re_(f_|_A))_._x_=_((Re_f)_|_A)_._x let x be set ; ::_thesis: ( x in dom ((Re f) | A) implies (Re (f | A)) . x = ((Re f) | A) . x ) assume A2: x in dom ((Re f) | A) ; ::_thesis: (Re (f | A)) . x = ((Re f) | A) . x then A3: x in (dom (Re f)) /\ A by RELAT_1:61; then A4: x in dom (Re f) by XBOOLE_0:def_4; A5: x in A by A3, XBOOLE_0:def_4; thus (Re (f | A)) . x = Re ((f | A) . x) by A1, A2, COMSEQ_3:def_3 .= Re (f . x) by A5, FUNCT_1:49 .= (Re f) . x by A4, COMSEQ_3:def_3 .= ((Re f) | A) . x by A5, FUNCT_1:49 ; ::_thesis: verum end; hence (Re f) | A = Re (f | A) by A1, FUNCT_1:2; ::_thesis: (Im f) | A = Im (f | A) dom ((Im f) | A) = (dom (Im f)) /\ A by RELAT_1:61 .= (dom f) /\ A by COMSEQ_3:def_4 ; then A6: dom ((Im f) | A) = dom (f | A) by RELAT_1:61 .= dom (Im (f | A)) by COMSEQ_3:def_4 ; now__::_thesis:_for_x_being_set_st_x_in_dom_((Im_f)_|_A)_holds_ (Im_(f_|_A))_._x_=_((Im_f)_|_A)_._x let x be set ; ::_thesis: ( x in dom ((Im f) | A) implies (Im (f | A)) . x = ((Im f) | A) . x ) assume A7: x in dom ((Im f) | A) ; ::_thesis: (Im (f | A)) . x = ((Im f) | A) . x then A8: x in (dom (Im f)) /\ A by RELAT_1:61; then A9: x in dom (Im f) by XBOOLE_0:def_4; A10: x in A by A8, XBOOLE_0:def_4; thus (Im (f | A)) . x = Im ((f | A) . x) by A6, A7, COMSEQ_3:def_4 .= Im (f . x) by A10, FUNCT_1:49 .= (Im f) . x by A9, COMSEQ_3:def_4 .= ((Im f) | A) . x by A10, FUNCT_1:49 ; ::_thesis: verum end; hence (Im f) | A = Im (f | A) by A6, FUNCT_1:2; ::_thesis: verum end; theorem Th8: :: MESFUN6C:8 for X being non empty set for f being PartFunc of X,COMPLEX holds f = (Re f) + ( (#) (Im f)) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds f = (Re f) + ( (#) (Im f)) let f be PartFunc of X,COMPLEX; ::_thesis: f = (Re f) + ( (#) (Im f)) A1: dom f = dom (Re f) by COMSEQ_3:def_3; A2: dom f = dom (Im f) by COMSEQ_3:def_4; A3: dom ((Re f) + ( (#) (Im f))) = (dom (Re f)) /\ (dom ( (#) (Im f))) by VALUED_1:def_1 .= (dom f) /\ (dom f) by A1, A2, VALUED_1:def_5 ; A4: dom ( (#) (Im f)) = dom (Im f) by VALUED_1:def_5; now__::_thesis:_for_x_being_set_st_x_in_dom_((Re_f)_+_(_(#)_(Im_f)))_holds_ ((Re_f)_+_(_(#)_(Im_f)))_._x_=_f_._x let x be set ; ::_thesis: ( x in dom ((Re f) + ( (#) (Im f))) implies ((Re f) + ( (#) (Im f))) . x = f . x ) assume A5: x in dom ((Re f) + ( (#) (Im f))) ; ::_thesis: ((Re f) + ( (#) (Im f))) . x = f . x then ((Re f) + ( (#) (Im f))) . x = ((Re f) . x) + (( (#) (Im f)) . x) by VALUED_1:def_1 .= (Re (f . x)) + (( (#) (Im f)) . x) by A1, A3, A5, COMSEQ_3:def_3 .= (Re (f . x)) + ( * ((Im f) . x)) by A2, A4, A3, A5, VALUED_1:def_5 .= (Re (f . x)) + ( * (Im (f . x))) by A2, A3, A5, COMSEQ_3:def_4 ; hence ((Re f) + ( (#) (Im f))) . x = f . x by COMPLEX1:13; ::_thesis: verum end; hence f = (Re f) + ( (#) (Im f)) by A3, FUNCT_1:2; ::_thesis: verum end; theorem :: MESFUN6C:9 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 A1: B c= A ; ::_thesis: ( not f is_measurable_on A or f is_measurable_on B ) assume A2: f is_measurable_on A ; ::_thesis: f is_measurable_on B then Im f is_measurable_on A by Def1; then A3: Im f is_measurable_on B by A1, MESFUNC6:16; Re f is_measurable_on A by A2, Def1; then Re f is_measurable_on B by A1, MESFUNC6:16; hence f is_measurable_on B by A3, Def1; ::_thesis: verum end; theorem :: MESFUN6C:10 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 that A1: f is_measurable_on A and A2: f is_measurable_on B ; ::_thesis: f is_measurable_on A \/ B A3: Im f is_measurable_on B by A2, Def1; Im f is_measurable_on A by A1, Def1; then A4: Im f is_measurable_on A \/ B by A3, MESFUNC6:17; A5: Re f is_measurable_on B by A2, Def1; Re f is_measurable_on A by A1, Def1; then Re f is_measurable_on A \/ B by A5, MESFUNC6:17; hence f is_measurable_on A \/ B by A4, Def1; ::_thesis: verum end; theorem :: MESFUN6C:11 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 that A1: f is_measurable_on A and A2: g is_measurable_on A ; ::_thesis: f + g is_measurable_on A A3: Im g is_measurable_on A by A2, Def1; Im f is_measurable_on A by A1, Def1; then (Im f) + (Im g) is_measurable_on A by A3, MESFUNC6:26; then A4: Im (f + g) is_measurable_on A by Th5; A5: Re g is_measurable_on A by A2, Def1; Re f is_measurable_on A by A1, Def1; then (Re f) + (Re g) is_measurable_on A by A5, MESFUNC6:26; then Re (f + g) is_measurable_on A by Th5; hence f + g is_measurable_on A by A4, Def1; ::_thesis: verum end; theorem :: MESFUN6C:12 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 A4: Im g is_measurable_on A by A2, Def1; A5: A c= dom (Re g) by A3, COMSEQ_3:def_3; A6: Re g is_measurable_on A by A2, Def1; A7: A c= dom (Im g) by A3, COMSEQ_3:def_4; Im f is_measurable_on A by A1, Def1; then (Im f) - (Im g) is_measurable_on A by A4, A7, MESFUNC6:29; then A8: Im (f - g) is_measurable_on A by Th6; Re f is_measurable_on A by A1, Def1; then (Re f) - (Re g) is_measurable_on A by A6, A5, MESFUNC6:29; then Re (f - g) is_measurable_on A by Th6; hence f - g is_measurable_on A by A8, Def1; ::_thesis: verum end; theorem :: MESFUN6C:13 for X being non empty set for Y being set for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds ( 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,COMPLEX st Y c= dom (f + g) holds ( 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,COMPLEX st Y c= dom (f + g) holds ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Y c= dom (f + g) implies ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) ) A1: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; assume A2: Y c= dom (f + g) ; ::_thesis: ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) then A3: dom ((f + g) | Y) = Y by RELAT_1:62; dom (g | Y) = (dom g) /\ Y by RELAT_1:61; then A4: dom (g | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28; dom (f | Y) = (dom f) /\ Y by RELAT_1:61; then A5: dom (f | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28; then A6: dom ((f | Y) + (g | Y)) = Y /\ Y by A4, VALUED_1:def_1; 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 A7: 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 A2, A3, A7, VALUED_1:def_1 .= ((f | Y) . x) + (g . x) by A3, A5, A7, FUNCT_1:47 .= ((f | Y) . x) + ((g | Y) . x) by A3, A4, A7, FUNCT_1:47 .= ((f | Y) + (g | Y)) . x by A3, A6, A7, VALUED_1:def_1 ; ::_thesis: verum end; hence ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A2, A6, FUNCT_1:2, RELAT_1:62; ::_thesis: verum end; theorem :: MESFUN6C:14 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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: A = (dom (Im f)) /\ B by A2, COMSEQ_3:def_4; Im f is_measurable_on B by A1, Def1; then (Im f) | B is_measurable_on A by A3, MESFUNC6:76; then A4: Im (f | B) is_measurable_on A by Th7; A5: A = (dom (Re f)) /\ B by A2, COMSEQ_3:def_3; Re f is_measurable_on B by A1, Def1; then (Re f) | B is_measurable_on A by A5, MESFUNC6:76; then Re (f | B) is_measurable_on A by Th7; hence f | B is_measurable_on A by A4, Def1; ::_thesis: verum end; theorem :: MESFUN6C:15 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX st dom f in S & dom g in S holds dom (f + g) in S let f, g be PartFunc of X,COMPLEX; ::_thesis: ( dom f in S & dom g in S implies dom (f + g) in S ) assume that A1: dom f in S and A2: dom g in S ; ::_thesis: dom (f + g) in S reconsider E1 = dom f, E2 = dom g as Element of S by A1, A2; dom (f + g) = E1 /\ E2 by VALUED_1:def_1; hence dom (f + g) in S ; ::_thesis: verum end; theorem :: MESFUN6C:16 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 ) then A2: dom (Re f) = A by COMSEQ_3:def_3; A3: dom (Im f) = A by A1, COMSEQ_3:def_4; hereby ::_thesis: ( f is_measurable_on A /\ B implies f is_measurable_on B ) assume A4: f is_measurable_on B ; ::_thesis: f is_measurable_on A /\ B then Im f is_measurable_on B by Def1; then A5: Im f is_measurable_on A /\ B by A3, MESFUNC6:80; Re f is_measurable_on B by A4, Def1; then Re f is_measurable_on A /\ B by A2, MESFUNC6:80; hence f is_measurable_on A /\ B by A5, Def1; ::_thesis: verum end; hereby ::_thesis: verum assume A6: f is_measurable_on A /\ B ; ::_thesis: f is_measurable_on B then Im f is_measurable_on A /\ B by Def1; then A7: Im f is_measurable_on B by A3, MESFUNC6:80; Re f is_measurable_on A /\ B by A6, Def1; then Re f is_measurable_on B by A2, MESFUNC6:80; hence f is_measurable_on B by A7, Def1; ::_thesis: verum end; end; theorem Th17: :: MESFUN6C:17 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for c being complex number for A being Element of S st f is_measurable_on A & A c= dom f holds c (#) 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,COMPLEX for c being complex number for A being Element of S st f is_measurable_on A & A c= dom f holds c (#) f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX for c being complex number for A being Element of S st f is_measurable_on A & A c= dom f holds c (#) f is_measurable_on A let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number for A being Element of S st f is_measurable_on A & A c= dom f holds c (#) f is_measurable_on A let c be complex number ; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds c (#) f is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies c (#) f is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: c (#) f is_measurable_on A A3: dom (Im f) = dom f by COMSEQ_3:def_4; A4: Im f is_measurable_on A by A1, Def1; then A5: (Re c) (#) (Im f) is_measurable_on A by A2, A3, MESFUNC6:21; A6: (Im c) (#) (Im f) is_measurable_on A by A2, A4, A3, MESFUNC6:21; A7: dom (Re f) = dom f by COMSEQ_3:def_3; A8: Re f is_measurable_on A by A1, Def1; then (Im c) (#) (Re f) is_measurable_on A by A2, A7, MESFUNC6:21; then ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) is_measurable_on A by A5, MESFUNC6:26; then A9: Im (c (#) f) is_measurable_on A by Th3; dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5; then A10: A c= dom ((Im c) (#) (Im f)) by A2, COMSEQ_3:def_4; (Re c) (#) (Re f) is_measurable_on A by A2, A8, A7, MESFUNC6:21; then ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) is_measurable_on A by A6, A10, MESFUNC6:29; then Re (c (#) f) is_measurable_on A by Th3; hence c (#) f is_measurable_on A by A9, Def1; ::_thesis: verum end; theorem :: MESFUN6C:18 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX st ex A being Element of S st dom f = A holds for c being complex number 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,COMPLEX st ex A being Element of S st dom f = A holds for c being complex number 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,COMPLEX st ex A being Element of S st dom f = A holds for c being complex number 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,COMPLEX; ::_thesis: ( ex A being Element of S st dom f = A implies for c being complex number 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 complex number 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 ; hereby ::_thesis: verum let c be complex number ; ::_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 ) A2: dom ((Re c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5; A3: dom ((Im c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5; dom (Re (c (#) f)) = dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) by Th3; then A4: dom (Re (c (#) f)) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f))) by VALUED_1:12; A5: dom ((Im c) (#) (Re f)) = dom (Re f) by VALUED_1:def_5; dom (Im (c (#) f)) = dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) by Th3; then A6: dom (Im (c (#) f)) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f))) by VALUED_1:def_1; A7: dom ((Re c) (#) (Im f)) = dom (Im f) by VALUED_1:def_5; A8: dom (Re f) = dom f by COMSEQ_3:def_3; A9: dom (Im f) = dom f by COMSEQ_3:def_4; assume A10: f is_measurable_on B ; ::_thesis: c (#) f is_measurable_on B then Im f is_measurable_on B by Def1; then A11: Im f is_measurable_on A /\ B by A1, A9, MESFUNC6:80; Re f is_measurable_on B by A10, Def1; then Re f is_measurable_on A /\ B by A1, A8, MESFUNC6:80; then f is_measurable_on A /\ B by A11, Def1; then A12: c (#) f is_measurable_on A /\ B by A1, Th17, XBOOLE_1:17; then Im (c (#) f) is_measurable_on A /\ B by Def1; then A13: Im (c (#) f) is_measurable_on B by A1, A8, A9, A5, A7, A6, MESFUNC6:80; Re (c (#) f) is_measurable_on A /\ B by A12, Def1; then Re (c (#) f) is_measurable_on B by A1, A8, A9, A2, A3, A4, MESFUNC6:80; hence c (#) f is_measurable_on B by A13, Def1; ::_thesis: verum end; 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,COMPLEX; predf is_integrable_on M means :Def2: :: MESFUN6C:def 2 ( Re f is_integrable_on M & Im f is_integrable_on M ); end; :: deftheorem Def2 defines is_integrable_on MESFUN6C:def_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,COMPLEX holds ( f is_integrable_on M iff ( Re f is_integrable_on M & Im f is_integrable_on M ) ); 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,COMPLEX; assume A1: f is_integrable_on M ; func Integral (M,f) -> complex number means :Def3: :: MESFUN6C:def 3 ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & it = R + (I * ) ); existence ex b1 being complex number ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b1 = R + (I * ) ) proof A2: Im f is_integrable_on M by A1, Def2; then A3: -infty < Integral (M,(Im f)) by MESFUNC6:90; A4: Re f is_integrable_on M by A1, Def2; then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90; A6: Integral (M,(Im f)) < +infty by A2, MESFUNC6:90; -infty < Integral (M,(Re f)) by A4, MESFUNC6:90; then reconsider R = Integral (M,(Re f)), I = Integral (M,(Im f)) as Real by A5, A3, A6, XXREAL_0:14; take R + (I * ) ; ::_thesis: ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * ) = R + (I * ) ) thus ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & R + (I * ) = R + (I * ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being complex number st ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b1 = R + (I * ) ) & ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b2 = R + (I * ) ) holds b1 = b2 ; end; :: deftheorem Def3 defines Integral MESFUN6C: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,COMPLEX st f is_integrable_on M holds for b5 being complex number holds ( b5 = Integral (M,f) iff ex R, I being Real st ( R = Integral (M,(Re f)) & I = Integral (M,(Im f)) & b5 = R + (I * ) ) ); Lm1: 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 holds ( max+ f is nonnegative & max- f is nonnegative ) 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 holds ( max+ f is nonnegative & max- f is nonnegative ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,ExtREAL holds ( max+ f is nonnegative & max- f is nonnegative ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL holds ( max+ f is nonnegative & max- f is nonnegative ) let f be PartFunc of X,ExtREAL; ::_thesis: ( max+ f is nonnegative & max- f is nonnegative ) A1: for x being set st x in dom (max- f) holds 0 <= (max- f) . x by MESFUNC2:13; for x being set st x in dom (max+ f) holds 0 <= (max+ f) . x by MESFUNC2:12; hence ( max+ f is nonnegative & max- f is nonnegative ) by A1, SUPINF_2:52; ::_thesis: verum end; theorem Th19: :: MESFUN6C:19 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 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 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,ExtREAL 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 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,ExtREAL 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 f | A is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,ExtREAL 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 f | A is_integrable_on M let f be PartFunc of X,ExtREAL; ::_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 f | A is_integrable_on M 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 f | A is_integrable_on M ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: M . A = 0 ; ::_thesis: f | A is_integrable_on M A3: dom f = dom (max+ f) by MESFUNC2:def_2; max+ f is nonnegative by Lm1; then integral+ (M,((max+ f) | A)) = 0 by A1, A2, A3, MESFUNC2:25, MESFUNC5:82; then A4: integral+ (M,(max+ (f | A))) < +infty by MESFUNC5:28; consider E being Element of S such that A5: E = dom f and A6: f is_measurable_on E by A1; A7: (dom f) /\ (A /\ E) = A /\ E by A5, XBOOLE_1:17, XBOOLE_1:28; A8: dom f = dom (max- f) by MESFUNC2:def_3; max- f is nonnegative by Lm1; then integral+ (M,((max- f) | A)) = 0 by A1, A2, A8, MESFUNC2:26, MESFUNC5:82; then A9: integral+ (M,(max- (f | A))) < +infty by MESFUNC5:28; A10: dom (f | A) = (dom f) /\ A by RELAT_1:61; f is_measurable_on A /\ E by A6, MESFUNC1:30, XBOOLE_1:17; then A11: f | (A /\ E) is_measurable_on A /\ E by A7, MESFUNC5:42; f | (A /\ E) = (f | A) /\ (f | E) by RELAT_1:79 .= (f | A) /\ f by A5, RELAT_1:69 .= f | A by RELAT_1:59, XBOOLE_1:28 ; hence f | A is_integrable_on M by A5, A11, A10, A4, A9, MESFUNC5:def_17; ::_thesis: verum end; theorem Th20: :: MESFUN6C:20 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 ex E being Element of S st ( E = dom f & f is_measurable_on E ) & M . A = 0 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 E, 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 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 E, 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 f | A is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,REAL for E, 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 f | A is_integrable_on M let f be PartFunc of X,REAL; ::_thesis: for E, 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 f | A is_integrable_on M let E, 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 f | A is_integrable_on M ) assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: M . A = 0 ; ::_thesis: f | A is_integrable_on M 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, MESFUNC6:def_1; then R_EAL (f | A) is_integrable_on M by A2, A3, Th19; hence f | A is_integrable_on M by MESFUNC6:def_4; ::_thesis: verum end; theorem :: MESFUN6C:21 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,COMPLEX 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 ( f | A is_integrable_on M & 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,COMPLEX 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 ( f | A is_integrable_on M & 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,COMPLEX 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 ( f | A is_integrable_on M & Integral (M,(f | A)) = 0 ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX 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 ( f | A is_integrable_on M & Integral (M,(f | A)) = 0 ) let f be PartFunc of X,COMPLEX; ::_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 ( f | A is_integrable_on M & 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 ( f | A is_integrable_on M & Integral (M,(f | A)) = 0 ) ) set g = f | A; assume that A1: ex E being Element of S st ( E = dom f & f is_measurable_on E ) and A2: M . A = 0 ; ::_thesis: ( f | A is_integrable_on M & 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; A5: dom (Im f) = dom f by COMSEQ_3:def_4; A6: Im f is_measurable_on E by A4, Def1; then A7: Integral (M,((Im f) | A)) = 0 by A2, A3, A5, MESFUNC6:88; (Im f) | A is_integrable_on M by A2, A3, A6, A5, Th20; then A8: Im (f | A) is_integrable_on M by Th7; A9: dom (Re f) = dom f by COMSEQ_3:def_3; A10: Im (f | A) = (Im f) | A by Th7; A11: Re f is_measurable_on E by A4, Def1; A12: Re (f | A) = (Re f) | A by Th7; then reconsider R = Integral (M,(Re (f | A))), I = Integral (M,(Im (f | A))) as Real by A2, A3, A11, A6, A9, A5, A10, MESFUNC6:88; (Re f) | A is_integrable_on M by A2, A3, A11, A9, Th20; then Re (f | A) is_integrable_on M by Th7; hence f | A is_integrable_on M by A8, Def2; ::_thesis: Integral (M,(f | A)) = 0 hence Integral (M,(f | A)) = R + (I * ) by Def3 .= 0 by A2, A3, A11, A9, A7, A12, A10, MESFUNC6:88 ; ::_thesis: verum end; theorem :: MESFUN6C:22 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,COMPLEX for E, A being Element of S st E = dom f & f is_integrable_on M & 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,COMPLEX for E, A being Element of S st E = dom f & f is_integrable_on M & 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,COMPLEX for E, A being Element of S st E = dom f & f is_integrable_on M & 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,COMPLEX for E, A being Element of S st E = dom f & f is_integrable_on M & M . A = 0 holds Integral (M,(f | (E \ A))) = Integral (M,f) let f be PartFunc of X,COMPLEX; ::_thesis: for E, A being Element of S st E = dom f & f is_integrable_on M & 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_integrable_on M & M . A = 0 implies Integral (M,(f | (E \ A))) = Integral (M,f) ) assume that A1: E = dom f and A2: f is_integrable_on M and A3: M . A = 0 ; ::_thesis: Integral (M,(f | (E \ A))) = Integral (M,f) set C = E \ A; A4: dom f = dom (Re f) by COMSEQ_3:def_3; A5: Im f is_integrable_on M by A2, Def2; then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4; then consider IE being Element of S such that A6: IE = dom (R_EAL (Im f)) and A7: R_EAL (Im f) is_measurable_on IE by MESFUNC5:def_17; A8: dom f = dom (Im f) by COMSEQ_3:def_4; A9: Integral (M,((Im f) | (E \ A))) = Integral (M,(Im (f | (E \ A)))) by Th7; Im f is_measurable_on IE by A7, MESFUNC6:def_1; then A10: Integral (M,(Im (f | (E \ A)))) = Integral (M,(Im f)) by A1, A3, A8, A6, A9, MESFUNC6:89; (Im f) | (E \ A) is_integrable_on M by A5, MESFUNC6:91; then A11: Im (f | (E \ A)) is_integrable_on M by Th7; then A12: -infty < Integral (M,(Im (f | (E \ A)))) by MESFUNC6:90; A13: Re f is_integrable_on M by A2, Def2; then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4; then consider RE being Element of S such that A14: RE = dom (R_EAL (Re f)) and A15: R_EAL (Re f) is_measurable_on RE by MESFUNC5:def_17; A16: Integral (M,((Re f) | (E \ A))) = Integral (M,(Re (f | (E \ A)))) by Th7; Re f is_measurable_on RE by A15, MESFUNC6:def_1; then A17: Integral (M,(Re (f | (E \ A)))) = Integral (M,(Re f)) by A1, A3, A4, A14, A16, MESFUNC6:89; (Re f) | (E \ A) is_integrable_on M by A13, MESFUNC6:91; then A18: Re (f | (E \ A)) is_integrable_on M by Th7; then A19: Integral (M,(Re (f | (E \ A)))) < +infty by MESFUNC6:90; A20: Integral (M,(Im (f | (E \ A)))) < +infty by A11, MESFUNC6:90; -infty < Integral (M,(Re (f | (E \ A)))) by A18, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (f | (E \ A)))), I2 = Integral (M,(Im (f | (E \ A)))) as Real by A19, A12, A20, XXREAL_0:14; f | (E \ A) is_integrable_on M by A18, A11, Def2; hence Integral (M,(f | (E \ A))) = R2 + (I2 * ) by Def3 .= Integral (M,f) by A2, A17, A10, Def3 ; ::_thesis: verum end; theorem Th23: :: MESFUN6C:23 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 A1: f is_integrable_on M ; ::_thesis: f | A is_integrable_on M then Im f is_integrable_on M by Def2; then (Im f) | A is_integrable_on M by MESFUNC6:91; then A2: Im (f | A) is_integrable_on M by Th7; Re f is_integrable_on M by A1, Def2; then (Re f) | A is_integrable_on M by MESFUNC6:91; then Re (f | A) is_integrable_on M by Th7; hence f | A is_integrable_on M by A2, Def2; ::_thesis: verum end; theorem :: MESFUN6C:24 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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))) A3: f | B is_integrable_on M by A1, Th23; then A4: Re (f | B) is_integrable_on M by Def2; then A5: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90; A6: Im (f | B) is_integrable_on M by A3, Def2; then A7: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90; A8: Integral (M,(Im (f | B))) < +infty by A6, MESFUNC6:90; -infty < Integral (M,(Re (f | B))) by A4, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (f | B))), I2 = Integral (M,(Im (f | B))) as Real by A5, A7, A8, XXREAL_0:14; A9: f | A is_integrable_on M by A1, Th23; then A10: Re (f | A) is_integrable_on M by Def2; then A11: Integral (M,(Re (f | A))) < +infty by MESFUNC6:90; set C = A \/ B; A12: f | (A \/ B) is_integrable_on M by A1, Th23; then A13: Re (f | (A \/ B)) is_integrable_on M by Def2; then A14: Integral (M,(Re (f | (A \/ B)))) < +infty by MESFUNC6:90; A15: Im (f | (A \/ B)) is_integrable_on M by A12, Def2; then A16: -infty < Integral (M,(Im (f | (A \/ B)))) by MESFUNC6:90; A17: Integral (M,(Im (f | (A \/ B)))) < +infty by A15, MESFUNC6:90; -infty < Integral (M,(Re (f | (A \/ B)))) by A13, MESFUNC6:90; then reconsider R3 = Integral (M,(Re (f | (A \/ B)))), I3 = Integral (M,(Im (f | (A \/ B)))) as Real by A14, A16, A17, XXREAL_0:14; A18: Integral (M,(f | (A \/ B))) = R3 + (I3 * ) by A12, Def3; A19: Im (f | A) is_integrable_on M by A9, Def2; then A20: -infty < Integral (M,(Im (f | A))) by MESFUNC6:90; A21: Integral (M,(Im (f | A))) < +infty by A19, MESFUNC6:90; -infty < Integral (M,(Re (f | A))) by A10, MESFUNC6:90; then reconsider R1 = Integral (M,(Re (f | A))), I1 = Integral (M,(Im (f | A))) as Real by A11, A20, A21, XXREAL_0:14; Im f is_integrable_on M by A1, Def2; then Integral (M,((Im f) | (A \/ B))) = (Integral (M,((Im f) | A))) + (Integral (M,((Im f) | B))) by A2, MESFUNC6:92; then Integral (M,((Im f) | (A \/ B))) = (Integral (M,(Im (f | A)))) + (Integral (M,((Im f) | B))) by Th7 .= (Integral (M,(Im (f | A)))) + (Integral (M,(Im (f | B)))) by Th7 ; then R_EAL I3 = (R_EAL I1) + (R_EAL I2) by Th7; then A22: I3 = I1 + I2 by SUPINF_2:1; Re f is_integrable_on M by A1, Def2; then Integral (M,((Re f) | (A \/ B))) = (Integral (M,((Re f) | A))) + (Integral (M,((Re f) | B))) by A2, MESFUNC6:92; then Integral (M,((Re f) | (A \/ B))) = (Integral (M,(Re (f | A)))) + (Integral (M,((Re f) | B))) by Th7 .= (Integral (M,(Re (f | A)))) + (Integral (M,(Re (f | B)))) by Th7 ; then R_EAL R3 = (R_EAL R1) + (R_EAL R2) by Th7; then R3 = R1 + R2 by SUPINF_2:1; then Integral (M,(f | (A \/ B))) = (R1 + (I1 * )) + (R2 + (I2 * )) by A22, A18; then Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (R2 + (I2 * )) by A9, Def3; hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A3, Def3; ::_thesis: verum end; theorem :: MESFUN6C:25 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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: Re f is_integrable_on M by A1, Def2; then A4: Integral (M,(Re f)) < +infty by MESFUNC6:90; A5: Im f is_integrable_on M by A1, Def2; then A6: -infty < Integral (M,(Im f)) by MESFUNC6:90; A7: Integral (M,(Im f)) < +infty by A5, MESFUNC6:90; -infty < Integral (M,(Re f)) by A3, MESFUNC6:90; then reconsider R = Integral (M,(Re f)), I = Integral (M,(Im f)) as Real by A4, A6, A7, XXREAL_0:14; A8: Integral (M,f) = R + (I * ) by A1, Def3; A9: f | B is_integrable_on M by A1, Th23; then A10: Re (f | B) is_integrable_on M by Def2; then A11: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90; A12: Im (f | B) is_integrable_on M by A9, Def2; then A13: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90; A14: Integral (M,(Im (f | B))) < +infty by A12, MESFUNC6:90; -infty < Integral (M,(Re (f | B))) by A10, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (f | B))), I2 = Integral (M,(Im (f | B))) as Real by A11, A13, A14, XXREAL_0:14; A15: f | A is_integrable_on M by A1, Th23; then A16: Re (f | A) is_integrable_on M by Def2; then A17: Integral (M,(Re (f | A))) < +infty by MESFUNC6:90; A18: Im (f | A) is_integrable_on M by A15, Def2; then A19: -infty < Integral (M,(Im (f | A))) by MESFUNC6:90; A20: Integral (M,(Im (f | A))) < +infty by A18, MESFUNC6:90; -infty < Integral (M,(Re (f | A))) by A16, MESFUNC6:90; then reconsider R1 = Integral (M,(Re (f | A))), I1 = Integral (M,(Im (f | A))) as Real by A17, A19, A20, XXREAL_0:14; dom f = dom (Im f) by COMSEQ_3:def_4; then Integral (M,(Im f)) = (Integral (M,((Im f) | A))) + (Integral (M,((Im f) | B))) by A2, A5, MESFUNC6:93; then Integral (M,(Im f)) = (Integral (M,(Im (f | A)))) + (Integral (M,((Im f) | B))) by Th7 .= (Integral (M,(Im (f | A)))) + (Integral (M,(Im (f | B)))) by Th7 ; then A21: I = I1 + I2 by SUPINF_2:1; dom f = dom (Re f) by COMSEQ_3:def_3; then Integral (M,(Re f)) = (Integral (M,((Re f) | A))) + (Integral (M,((Re f) | B))) by A2, A3, MESFUNC6:93; then Integral (M,(Re f)) = (Integral (M,(Re (f | A)))) + (Integral (M,((Re f) | B))) by Th7 .= (Integral (M,(Re (f | A)))) + (Integral (M,(Re (f | B)))) by Th7 ; then R = R1 + R2 by SUPINF_2:1; then Integral (M,f) = (R1 + (I1 * )) + (R2 + (I2 * )) by A21, A8; then Integral (M,f) = (Integral (M,(f | A))) + (R2 + (I2 * )) by A15, Def3; hence ( f | A is_integrable_on M & Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) ) by A1, A9, Def3, Th23; ::_thesis: verum end; definition let k be real number ; let X be non empty set ; let f be PartFunc of X,REAL; funcf to_power k -> PartFunc of X,REAL means :Def4: :: MESFUN6C:def 4 ( dom it = dom f & ( for x being Element of X st x in dom it holds it . x = (f . x) to_power k ) ); existence ex b1 being PartFunc of X,REAL st ( dom b1 = dom f & ( for x being Element of X st x in dom b1 holds b1 . x = (f . x) to_power k ) ) proof defpred S1[ set , set ] means ( $1 in dom f & $2 = (f . $1) to_power k ); consider F being PartFunc of X,REAL such that A1: for z being Element of X holds ( z in dom F iff ex c being Element of REAL st S1[z,c] ) and A2: for z being Element of X st z in dom F holds S1[z,F . z] from SEQ_1:sch_2(); take F ; ::_thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds F . x = (f . x) to_power k ) ) now__::_thesis:_for_z_being_Element_of_X_holds_ (_(_z_in_dom_f_implies_z_in_dom_F_)_&_(_z_in_dom_F_implies_z_in_dom_f_)_) let z be Element of X; ::_thesis: ( ( z in dom f implies z in dom F ) & ( z in dom F implies z in dom f ) ) hereby ::_thesis: ( z in dom F implies z in dom f ) A3: (f . z) to_power k is Element of REAL by XREAL_0:def_1; assume z in dom f ; ::_thesis: z in dom F hence z in dom F by A1, A3; ::_thesis: verum end; hereby ::_thesis: verum assume z in dom F ; ::_thesis: z in dom f then ex c being Element of REAL st S1[z,c] by A1; hence z in dom f ; ::_thesis: verum end; end; hence dom F = dom f by SUBSET_1:3; ::_thesis: for x being Element of X st x in dom F holds F . x = (f . x) to_power k thus for x being Element of X st x in dom F holds F . x = (f . x) to_power k by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,REAL st dom b1 = dom f & ( for x being Element of X st x in dom b1 holds b1 . x = (f . x) to_power k ) & dom b2 = dom f & ( for x being Element of X st x in dom b2 holds b2 . x = (f . x) to_power k ) holds b1 = b2 proof deffunc H1( set ) -> set = (f . $1) to_power k; thus for h, g being PartFunc of X,REAL st dom h = dom f & ( for z being Element of X st z in dom h holds h . z = H1(z) ) & dom g = dom f & ( for z being Element of X st z in dom g holds g . z = H1(z) ) holds h = g from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem Def4 defines to_power MESFUN6C:def_4_:_ for k being real number for X being non empty set for f, b4 being PartFunc of X,REAL holds ( b4 = f to_power k iff ( dom b4 = dom f & ( for x being Element of X st x in dom b4 holds b4 . x = (f . x) to_power k ) ) ); registration let X be non empty set ; cluster Relation-like X -defined REAL -valued Function-like V33() V34() V35() nonnegative for Element of K6(K7(X,REAL)); existence ex b1 being PartFunc of X,REAL st b1 is nonnegative proof reconsider f = {} as Function ; reconsider f = f as PartFunc of X,REAL by RELSET_1:12; take f ; ::_thesis: f is nonnegative let x be Element of ExtREAL ; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( not x in rng f or 0. <= x ) thus ( not x in rng f or 0. <= x ) ; ::_thesis: verum end; end; registration let k be real non negative number ; let X be non empty set ; let f be nonnegative PartFunc of X,REAL; clusterf to_power k -> nonnegative ; coherence f to_power k is nonnegative proof now__::_thesis:_for_x_being_set_st_x_in_dom_(f_to_power_k)_holds_ 0_<=_(f_to_power_k)_._x let x be set ; ::_thesis: ( x in dom (f to_power k) implies 0 <= (f to_power k) . b1 ) assume A1: x in dom (f to_power k) ; ::_thesis: 0 <= (f to_power k) . b1 percases ( k = 0 or k > 0 ) ; suppose k = 0 ; ::_thesis: 0 <= (f to_power k) . b1 then (f . x) to_power k = 1 by POWER:24; hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum end; supposeA2: k > 0 ; ::_thesis: 0 <= (f to_power k) . b1 percases ( 0 < f . x or 0 = f . x ) by MESFUNC6:51; suppose 0 < f . x ; ::_thesis: 0 <= (f to_power k) . b1 then 0 < (f . x) to_power k by POWER:34; hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum end; suppose 0 = f . x ; ::_thesis: 0 <= (f to_power k) . b1 then 0 = (f . x) to_power k by A2, POWER:def_2; hence 0 <= (f to_power k) . x by A1, Def4; ::_thesis: verum end; end; end; end; end; hence f to_power k is nonnegative by MESFUNC6:52; ::_thesis: verum end; end; theorem Th26: :: MESFUN6C:26 for k being real number for X being non empty set for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative & 0 <= k holds f to_power k is nonnegative ; theorem Th27: :: MESFUN6C:27 for x being set for X being non empty set for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative holds (f . x) to_power (1 / 2) = sqrt (f . x) proof let x be set ; ::_thesis: for X being non empty set for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative holds (f . x) to_power (1 / 2) = sqrt (f . x) let X be non empty set ; ::_thesis: for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative holds (f . x) to_power (1 / 2) = sqrt (f . x) let S be SigmaField of X; ::_thesis: for E being Element of S for f being PartFunc of X,REAL st f is nonnegative holds (f . x) to_power (1 / 2) = sqrt (f . x) let E be Element of S; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative holds (f . x) to_power (1 / 2) = sqrt (f . x) let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative implies (f . x) to_power (1 / 2) = sqrt (f . x) ) assume f is nonnegative ; ::_thesis: (f . x) to_power (1 / 2) = sqrt (f . x) then A1: 0 <= f . x by MESFUNC6:51; hence (f . x) to_power (1 / 2) = 2 -root (f . x) by POWER:45 .= 2 -Root (f . x) by A1, POWER:def_1 .= sqrt (f . x) by A1, PREPOWER:32 ; ::_thesis: verum end; theorem Th28: :: MESFUN6C:28 for X being non empty set for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let S be SigmaField of X; ::_thesis: for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let A be Element of S; ::_thesis: for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let a be Real; ::_thesis: ( A c= dom f implies A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) ) now__::_thesis:_for_x_being_set_st_x_in_A_/\_(less_dom_(f,a))_holds_ x_in_A_\_(A_/\_(great_eq_dom_(f,a))) let x be set ; ::_thesis: ( x in A /\ (less_dom (f,a)) implies x in A \ (A /\ (great_eq_dom (f,a))) ) assume A1: x in A /\ (less_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_eq_dom (f,a))) then x in less_dom (f,a) by XBOOLE_0:def_4; then ex y being Real st ( y = f . x & y < a ) by MESFUNC6:3; then for y1 being Real holds ( not y1 = f . x or not a <= y1 ) ; then not x in great_eq_dom (f,a) by MESFUNC6:6; then A2: not x in A /\ (great_eq_dom (f,a)) by XBOOLE_0:def_4; x in A by A1, XBOOLE_0:def_4; hence x in A \ (A /\ (great_eq_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum end; then A3: A /\ (less_dom (f,a)) c= A \ (A /\ (great_eq_dom (f,a))) by TARSKI:def_3; assume A4: A c= dom f ; ::_thesis: A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(great_eq_dom_(f,a)))_holds_ x_in_A_/\_(less_dom_(f,a)) let x be set ; ::_thesis: ( x in A \ (A /\ (great_eq_dom (f,a))) implies x in A /\ (less_dom (f,a)) ) assume A5: x in A \ (A /\ (great_eq_dom (f,a))) ; ::_thesis: x in A /\ (less_dom (f,a)) then A6: x in A by XBOOLE_0:def_5; not x in A /\ (great_eq_dom (f,a)) by A5, XBOOLE_0:def_5; then not x in great_eq_dom (f,a) by A6, XBOOLE_0:def_4; then not a <= f . x by A4, A6, MESFUNC6:6; then x in less_dom (f,a) by A4, A6, MESFUNC6:3; hence x in A /\ (less_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (great_eq_dom (f,a))) c= A /\ (less_dom (f,a)) by TARSKI:def_3; hence A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: MESFUN6C:29 for k being real number for X being non empty set for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds f to_power k is_measurable_on E proof let k be real number ; ::_thesis: for X being non empty set for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds f to_power k is_measurable_on E let X be non empty set ; ::_thesis: for S being SigmaField of X for E being Element of S for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds f to_power k is_measurable_on E let S be SigmaField of X; ::_thesis: for E being Element of S for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds f to_power k is_measurable_on E let E be Element of S; ::_thesis: for f being PartFunc of X,REAL st f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E holds f to_power k is_measurable_on E let f be PartFunc of X,REAL; ::_thesis: ( f is nonnegative & 0 <= k & E c= dom f & f is_measurable_on E implies f to_power k is_measurable_on E ) reconsider k1 = k as Real by XREAL_0:def_1; assume that A1: f is nonnegative and A2: 0 <= k and A3: E c= dom f and A4: f is_measurable_on E ; ::_thesis: f to_power k is_measurable_on E A5: dom (f to_power k) = dom f by Def4; percases ( k = 0 or k > 0 ) by A2; supposeA6: k = 0 ; ::_thesis: f to_power k is_measurable_on E A7: E c= dom (f to_power k) by A3, Def4; now__::_thesis:_for_r_being_real_number_holds_E_/\_(less_dom_((f_to_power_k),r))_in_S let r be real number ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S reconsider r1 = r as Real by XREAL_0:def_1; percases ( r <= 1 or 1 < r ) ; supposeA8: r <= 1 ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S now__::_thesis:_for_x_being_set_st_x_in_E_holds_ x_in_great_eq_dom_((f_to_power_k),r1) let x be set ; ::_thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) ) assume A9: x in E ; ::_thesis: x in great_eq_dom ((f to_power k),r1) then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4; then r <= (f to_power k) . x by A6, A8, POWER:24; hence x in great_eq_dom ((f to_power k),r1) by A3, A5, A9, MESFUNC6:6; ::_thesis: verum end; then E c= great_eq_dom ((f to_power k),r) by TARSKI:def_3; then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28; then E /\ (less_dom ((f to_power k),r1)) = E \ E by A7, Th28; hence E /\ (less_dom ((f to_power k),r)) in S ; ::_thesis: verum end; supposeA10: 1 < r ; ::_thesis: E /\ (less_dom ((f to_power k),b1)) in S now__::_thesis:_for_x_being_set_st_x_in_E_holds_ x_in_less_dom_((f_to_power_k),r) let x be set ; ::_thesis: ( x in E implies x in less_dom ((f to_power k),r) ) assume A11: x in E ; ::_thesis: x in less_dom ((f to_power k),r) then (f to_power k) . x = (f . x) to_power k by A3, A5, Def4; then (f to_power k) . x < r by A6, A10, POWER:24; hence x in less_dom ((f to_power k),r) by A3, A5, A11, MESFUNC6:3; ::_thesis: verum end; then E c= less_dom ((f to_power k),r) by TARSKI:def_3; then E /\ (less_dom ((f to_power k),r)) = E by XBOOLE_1:28; hence E /\ (less_dom ((f to_power k),r)) in S ; ::_thesis: verum end; end; end; hence f to_power k is_measurable_on E by MESFUNC6:12; ::_thesis: verum end; supposeA12: k > 0 ; ::_thesis: f to_power k is_measurable_on E for r being real number holds E /\ (great_eq_dom ((f to_power k),r)) in S proof let r be real number ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S reconsider r1 = r as Real by XREAL_0:def_1; percases ( r1 <= 0 or 0 < r1 ) ; supposeA13: r1 <= 0 ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S now__::_thesis:_for_x_being_set_st_x_in_E_holds_ x_in_great_eq_dom_((f_to_power_k),r1) let x be set ; ::_thesis: ( x in E implies x in great_eq_dom ((f to_power k),r1) ) assume x in E ; ::_thesis: x in great_eq_dom ((f to_power k),r1) then x in dom f by A3; then A14: x in dom (f to_power k) by Def4; 0 <= (f to_power k) . x by A1, A12, MESFUNC6:51; hence x in great_eq_dom ((f to_power k),r1) by A13, A14, MESFUNC6:6; ::_thesis: verum end; then E c= great_eq_dom ((f to_power k),r) by TARSKI:def_3; then E /\ (great_eq_dom ((f to_power k),r)) = E by XBOOLE_1:28; hence E /\ (great_eq_dom ((f to_power k),r)) in S ; ::_thesis: verum end; supposeA15: 0 < r1 ; ::_thesis: E /\ (great_eq_dom ((f to_power k),r)) in S A16: now__::_thesis:_for_x_being_set_st_x_in_great_eq_dom_(f,(r1_to_power_(1_/_k)))_holds_ x_in_great_eq_dom_((f_to_power_k),r1) set R = r to_power (1 / k); let x be set ; ::_thesis: ( x in great_eq_dom (f,(r1 to_power (1 / k))) implies x in great_eq_dom ((f to_power k),r1) ) A17: 0 < r to_power (1 / k) by A15, POWER:34; assume A18: x in great_eq_dom (f,(r1 to_power (1 / k))) ; ::_thesis: x in great_eq_dom ((f to_power k),r1) then A19: x in dom (f to_power k) by A5, MESFUNC6:6; (r to_power (1 / k)) to_power k = r to_power ((1 / k) * k) by A15, POWER:33; then A20: (r to_power (1 / k)) to_power k = r to_power 1 by A12, XCMPLX_1:87; ex y being Real st ( y = f . x & r1 to_power (1 / k) <= y ) by A18, MESFUNC6:6; then r1 to_power 1 <= (f . x) to_power k1 by A12, A17, A20, HOLDER_1:3; then r <= (f . x) to_power k by POWER:25; then r <= (f to_power k) . x by A19, Def4; hence x in great_eq_dom ((f to_power k),r1) by A19, MESFUNC6:6; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_great_eq_dom_((f_to_power_k),r1)_holds_ x_in_great_eq_dom_(f,(r1_to_power_(1_/_k))) let x be set ; ::_thesis: ( x in great_eq_dom ((f to_power k),r1) implies x in great_eq_dom (f,(r1 to_power (1 / k))) ) assume A21: x in great_eq_dom ((f to_power k),r1) ; ::_thesis: x in great_eq_dom (f,(r1 to_power (1 / k))) then A22: x in dom (f to_power k) by MESFUNC6:6; 0 <= f . x by A1, MESFUNC6:51; then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power ((k1 * 1) / k1) by A12, HOLDER_1:2; then ((f . x) to_power k1) to_power (1 / k1) = (f . x) to_power 1 by A12, XCMPLX_1:87; then A23: ((f . x) to_power k) to_power (1 / k) = f . x by POWER:25; ex y2 being Real st ( y2 = (f to_power k) . x & r1 <= y2 ) by A21, MESFUNC6:6; then r <= (f . x) to_power k by A22, Def4; then r to_power (1 / k1) <= ((f . x) to_power k1) to_power (1 / k1) by A12, A15, HOLDER_1:3; hence x in great_eq_dom (f,(r1 to_power (1 / k))) by A5, A22, A23, MESFUNC6:6; ::_thesis: verum end; then E /\ (great_eq_dom ((f to_power k),r1)) = E /\ (great_eq_dom (f,(r1 to_power (1 / k)))) by A16, TARSKI:1; hence E /\ (great_eq_dom ((f to_power k),r)) in S by A3, A4, MESFUNC6:13; ::_thesis: verum end; end; end; hence f to_power k is_measurable_on E by A3, A5, MESFUNC6:13; ::_thesis: verum end; end; end; theorem Th30: :: MESFUN6C:30 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for A being Element of S st f is_measurable_on A & A c= dom f 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,COMPLEX for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let f be PartFunc of X,COMPLEX; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds |.f.| is_measurable_on A let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies |.f.| is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: |.f.| is_measurable_on A A3: dom (Im f) = dom f by COMSEQ_3:def_4; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_|.(Im_f).|_holds_ 0_<=_|.(Im_f).|_._x let x be set ; ::_thesis: ( x in dom |.(Im f).| implies 0 <= |.(Im f).| . x ) assume x in dom |.(Im f).| ; ::_thesis: 0 <= |.(Im f).| . x then |.(Im f).| . x = |.((Im f) . x).| by VALUED_1:def_11; hence 0 <= |.(Im f).| . x by COMPLEX1:46; ::_thesis: verum end; then A5: |.(Im f).| to_power 2 is nonnegative by Th26, MESFUNC6:52; A6: dom |.(Im f).| = dom (Im f) by VALUED_1:def_11; then A7: dom (|.(Im f).| to_power 2) = dom f by A3, Def4; Im f is_measurable_on A by A1, Def1; then |.(Im f).| is_measurable_on A by A2, A3, MESFUNC6:48; then A8: |.(Im f).| to_power 2 is_measurable_on A by A2, A6, A3, A4, Th29, MESFUNC6:52; A9: dom (Re f) = dom f by COMSEQ_3:def_3; A10: now__::_thesis:_for_x_being_set_st_x_in_dom_|.(Re_f).|_holds_ 0_<=_|.(Re_f).|_._x let x be set ; ::_thesis: ( x in dom |.(Re f).| implies 0 <= |.(Re f).| . x ) A11: 0 <= |.((Re f) . x).| by COMPLEX1:46; assume x in dom |.(Re f).| ; ::_thesis: 0 <= |.(Re f).| . x hence 0 <= |.(Re f).| . x by A11, VALUED_1:def_11; ::_thesis: verum end; then A12: |.(Re f).| to_power 2 is nonnegative by Th26, MESFUNC6:52; set F = (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2); A13: dom |.f.| = dom f by VALUED_1:def_11; A14: dom |.(Re f).| = dom (Re f) by VALUED_1:def_11; then A15: dom (|.(Re f).| to_power 2) = dom f by A9, Def4; A16: dom ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) = (dom (|.(Re f).| to_power 2)) /\ (dom (|.(Im f).| to_power 2)) by VALUED_1:def_1; then A17: dom |.f.| = dom (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) by A13, A15, A7, Def4; now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_ |.f.|_._x_=_(((|.(Re_f).|_to_power_2)_+_(|.(Im_f).|_to_power_2))_to_power_(1_/_2))_._x let x be set ; ::_thesis: ( x in dom |.f.| implies |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x ) assume A18: x in dom |.f.| ; ::_thesis: |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x then (|.(Re f).| to_power 2) . x = (|.(Re f).| . x) to_power 2 by A13, A15, Def4; then (|.(Re f).| to_power 2) . x = |.((Re f) . x).| to_power 2 by A14, A13, A9, A18, VALUED_1:def_11; then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| to_power 2 by A13, A9, A18, COMSEQ_3:def_3; then (|.(Re f).| to_power 2) . x = |.(Re (f . x)).| ^2 by POWER:46; then A19: (|.(Re f).| to_power 2) . x = (Re (f . x)) ^2 by COMPLEX1:75; (|.(Im f).| to_power 2) . x = (|.(Im f).| . x) to_power 2 by A13, A7, A18, Def4; then (|.(Im f).| to_power 2) . x = |.((Im f) . x).| to_power 2 by A6, A13, A3, A18, VALUED_1:def_11; then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| to_power 2 by A13, A3, A18, COMSEQ_3:def_4; then (|.(Im f).| to_power 2) . x = |.(Im (f . x)).| ^2 by POWER:46; then A20: (|.(Im f).| to_power 2) . x = (Im (f . x)) ^2 by COMPLEX1:75; (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) to_power (1 / 2) = sqrt (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) . x) by A12, A5, Th27, MESFUNC6:56 .= sqrt (((Re (f . x)) ^2) + ((Im (f . x)) ^2)) by A13, A16, A15, A7, A18, A19, A20, VALUED_1:def_1 ; then (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x = |.(f . x).| by A17, A18, Def4; hence |.f.| . x = (((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2)) . x by A18, VALUED_1:def_11; ::_thesis: verum end; then A21: |.f.| = ((|.(Re f).| to_power 2) + (|.(Im f).| to_power 2)) to_power (1 / 2) by A17, FUNCT_1:2; Re f is_measurable_on A by A1, Def1; then |.(Re f).| is_measurable_on A by A2, A9, MESFUNC6:48; then |.(Re f).| to_power 2 is_measurable_on A by A2, A14, A9, A10, Th29, MESFUNC6:52; then (|.(Re f).| to_power 2) + (|.(Im f).| to_power 2) is_measurable_on A by A8, MESFUNC6:26; hence |.f.| is_measurable_on A by A2, A12, A5, A16, A15, A7, A21, Th29, MESFUNC6:56; ::_thesis: verum end; theorem Th31: :: MESFUN6C:31 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff |.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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff |.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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff |.f.| is_integrable_on M ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) holds ( f is_integrable_on M iff |.f.| is_integrable_on M ) let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) implies ( f is_integrable_on M iff |.f.| is_integrable_on M ) ) A1: dom (|.(Re f).| + |.(Im f).|) = (dom |.(Re f).|) /\ (dom |.(Im f).|) by VALUED_1:def_1; A2: dom |.(Re f).| = dom (Re f) by VALUED_1:def_11; A3: dom |.(Im f).| = dom (Im f) by VALUED_1:def_11; A4: dom |.f.| = dom f by VALUED_1:def_11; assume ex A being Element of S st ( A = dom f & f is_measurable_on A ) ; ::_thesis: ( f is_integrable_on M iff |.f.| is_integrable_on M ) then consider A being Element of S such that A5: A = dom f and A6: f is_measurable_on A ; A7: dom (Re f) = A by A5, COMSEQ_3:def_3; A8: Im f is_measurable_on A by A6, Def1; A9: Re f is_measurable_on A by A6, Def1; A10: dom (Im f) = A by A5, COMSEQ_3:def_4; A11: |.f.| is_measurable_on A by A5, A6, Th30; hereby ::_thesis: ( |.f.| is_integrable_on M implies f is_integrable_on M ) A12: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_|.f.|_holds_ |.(|.f.|_._x).|_<=_(|.(Re_f).|_+_|.(Im_f).|)_._x let x be Element of X; ::_thesis: ( x in dom |.f.| implies |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x ) assume A13: x in dom |.f.| ; ::_thesis: |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x then A14: |.f.| . x = |.(f . x).| by VALUED_1:def_11; A15: |.((Im f) . x).| = |.(Im f).| . x by A5, A10, A3, A4, A13, VALUED_1:def_11; A16: |.((Re f) . x).| = |.(Re f).| . x by A5, A7, A2, A4, A13, VALUED_1:def_11; A17: (Im f) . x = Im (f . x) by A5, A10, A4, A13, COMSEQ_3:def_4; A18: (Re f) . x = Re (f . x) by A5, A7, A4, A13, COMSEQ_3:def_3; (|.(Re f).| + |.(Im f).|) . x = (|.(Re f).| . x) + (|.(Im f).| . x) by A5, A7, A10, A1, A2, A3, A4, A13, VALUED_1:def_1; hence |.(|.f.| . x).| <= (|.(Re f).| + |.(Im f).|) . x by A18, A17, A14, A16, A15, COMPLEX1:78; ::_thesis: verum end; assume A19: f is_integrable_on M ; ::_thesis: |.f.| is_integrable_on M then Im f is_integrable_on M by Def2; then A20: |.(Im f).| is_integrable_on M by A10, A8, MESFUNC6:94; Re f is_integrable_on M by A19, Def2; then |.(Re f).| is_integrable_on M by A7, A9, MESFUNC6:94; then |.(Re f).| + |.(Im f).| is_integrable_on M by A20, MESFUNC6:100; hence |.f.| is_integrable_on M by A5, A7, A10, A1, A2, A3, A4, A11, A12, MESFUNC6:96; ::_thesis: verum end; hereby ::_thesis: verum assume A21: |.f.| is_integrable_on M ; ::_thesis: f is_integrable_on M now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Im_f)_holds_ |.((Im_f)_._x).|_<=_|.f.|_._x let x be Element of X; ::_thesis: ( x in dom (Im f) implies |.((Im f) . x).| <= |.f.| . x ) A22: |.(Im (f . x)).| <= |.(f . x).| by COMPLEX1:79; assume A23: x in dom (Im f) ; ::_thesis: |.((Im f) . x).| <= |.f.| . x then |.f.| . x = |.(f . x).| by A5, A10, A4, VALUED_1:def_11; hence |.((Im f) . x).| <= |.f.| . x by A23, A22, COMSEQ_3:def_4; ::_thesis: verum end; then A24: Im f is_integrable_on M by A5, A10, A8, A4, A21, MESFUNC6:96; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Re_f)_holds_ |.((Re_f)_._x).|_<=_|.f.|_._x let x be Element of X; ::_thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x ) A25: |.(Re (f . x)).| <= |.(f . x).| by COMPLEX1:79; assume A26: x in dom (Re f) ; ::_thesis: |.((Re f) . x).| <= |.f.| . x then |.f.| . x = |.(f . x).| by A5, A7, A4, VALUED_1:def_11; hence |.((Re f) . x).| <= |.f.| . x by A26, A25, COMSEQ_3:def_3; ::_thesis: verum end; then Re f is_integrable_on M by A5, A7, A9, A4, A21, MESFUNC6:96; hence f is_integrable_on M by A24, Def2; ::_thesis: verum end; end; theorem :: MESFUN6C:32 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX st f is_integrable_on M & g is_integrable_on M holds dom (f + g) in S let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies dom (f + g) in S ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: dom (f + g) in S A3: Re g is_integrable_on M by A2, Def2; A4: Im g is_integrable_on M by A2, Def2; Im f is_integrable_on M by A1, Def2; then dom ((Im f) + (Im g)) in S by A4, MESFUNC6:99; then A5: dom (Im (f + g)) in S by Th5; Re f is_integrable_on M by A1, Def2; then dom ((Re f) + (Re g)) in S by A3, MESFUNC6:99; then A6: dom (Re (f + g)) in S by Th5; dom ( (#) (Im (f + g))) = dom (Im (f + g)) by VALUED_1:def_5; then dom ((Re (f + g)) + ( (#) (Im (f + g)))) = (dom (Re (f + g))) /\ (dom (Im (f + g))) by VALUED_1:def_1; then dom ((Re (f + g)) + ( (#) (Im (f + g)))) in S by A6, A5, FINSUB_1:def_2; hence dom (f + g) in S by Th8; ::_thesis: verum end; theorem Th33: :: MESFUN6C:33 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: f + g is_integrable_on M A3: Im g is_integrable_on M by A2, Def2; Im f is_integrable_on M by A1, Def2; then (Im f) + (Im g) is_integrable_on M by A3, MESFUNC6:100; then A4: Im (f + g) is_integrable_on M by Th5; A5: Re g is_integrable_on M by A2, Def2; Re f is_integrable_on M by A1, Def2; then (Re f) + (Re g) is_integrable_on M by A5, MESFUNC6:100; then Re (f + g) is_integrable_on M by Th5; hence f + g is_integrable_on M by A4, Def2; ::_thesis: verum end; theorem Th34: :: MESFUN6C:34 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 that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M R_EAL g is_integrable_on M by A2, MESFUNC6:def_4; then (- 1) (#) (R_EAL g) is_integrable_on M by MESFUNC5:110; then - (R_EAL g) is_integrable_on M by MESFUNC2:9; then A3: R_EAL (- g) is_integrable_on M by MESFUNC6:28; R_EAL f is_integrable_on M by A1, MESFUNC6:def_4; then (R_EAL f) + (R_EAL (- g)) is_integrable_on M by A3, MESFUNC5:108; then R_EAL (f - g) is_integrable_on M by MESFUNC6:23; hence f - g is_integrable_on M by MESFUNC6:def_4; ::_thesis: verum end; theorem :: MESFUN6C:35 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f - g is_integrable_on M ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M A3: Im g is_integrable_on M by A2, Def2; Im f is_integrable_on M by A1, Def2; then (Im f) - (Im g) is_integrable_on M by A3, Th34; then A4: Im (f - g) is_integrable_on M by Th6; A5: Re g is_integrable_on M by A2, Def2; Re f is_integrable_on M by A1, Def2; then (Re f) - (Re g) is_integrable_on M by A5, Th34; then Re (f - g) is_integrable_on M by Th6; hence f - g is_integrable_on M by A4, Def2; ::_thesis: verum end; theorem Th36: :: MESFUN6C:36 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) A3: Re g is_integrable_on M by A2, Def2; Re f is_integrable_on M by A1, Def2; then consider E being Element of S such that A4: E = (dom (Re f)) /\ (dom (Re g)) and A5: Integral (M,((Re f) + (Re g))) = (Integral (M,((Re f) | E))) + (Integral (M,((Re g) | E))) by A3, MESFUNC6:101; A6: f | E is_integrable_on M by A1, Th23; then A7: Re (f | E) is_integrable_on M by Def2; then A8: Integral (M,(Re (f | E))) < +infty by MESFUNC6:90; A9: Im (f | E) is_integrable_on M by A6, Def2; then A10: -infty < Integral (M,(Im (f | E))) by MESFUNC6:90; A11: Integral (M,(Im (f | E))) < +infty by A9, MESFUNC6:90; -infty < Integral (M,(Re (f | E))) by A7, MESFUNC6:90; then reconsider R1 = Integral (M,(Re (f | E))), I1 = Integral (M,(Im (f | E))) as Real by A8, A10, A11, XXREAL_0:14; A12: dom f = dom (Re f) by COMSEQ_3:def_3; A13: Im g is_integrable_on M by A2, Def2; Im f is_integrable_on M by A1, Def2; then A14: ex Ei being Element of S st ( Ei = (dom (Im f)) /\ (dom (Im g)) & Integral (M,((Im f) + (Im g))) = (Integral (M,((Im f) | Ei))) + (Integral (M,((Im g) | Ei))) ) by A13, MESFUNC6:101; A15: Integral (M,((Im f) + (Im g))) = Integral (M,(Im (f + g))) by Th5; A16: f + g is_integrable_on M by A1, A2, Th33; then A17: Re (f + g) is_integrable_on M by Def2; then A18: Integral (M,(Re (f + g))) < +infty by MESFUNC6:90; A19: Im (f + g) is_integrable_on M by A16, Def2; then A20: -infty < Integral (M,(Im (f + g))) by MESFUNC6:90; A21: Integral (M,(Im (f + g))) < +infty by A19, MESFUNC6:90; -infty < Integral (M,(Re (f + g))) by A17, MESFUNC6:90; then reconsider R = Integral (M,(Re (f + g))), I = Integral (M,(Im (f + g))) as Real by A18, A20, A21, XXREAL_0:14; A22: Integral (M,(f + g)) = R + (I * ) by A16, Def3; A23: dom g = dom (Im g) by COMSEQ_3:def_4; A24: g | E is_integrable_on M by A2, Th23; then A25: Re (g | E) is_integrable_on M by Def2; then A26: Integral (M,(Re (g | E))) < +infty by MESFUNC6:90; A27: Im (g | E) is_integrable_on M by A24, Def2; then A28: -infty < Integral (M,(Im (g | E))) by MESFUNC6:90; A29: Integral (M,(Im (g | E))) < +infty by A27, MESFUNC6:90; -infty < Integral (M,(Re (g | E))) by A25, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (g | E))), I2 = Integral (M,(Im (g | E))) as Real by A26, A28, A29, XXREAL_0:14; A30: dom g = dom (Re g) by COMSEQ_3:def_3; Integral (M,((Re f) + (Re g))) = Integral (M,(Re (f + g))) by Th5; then Integral (M,(Re (f + g))) = (Integral (M,(Re (f | E)))) + (Integral (M,((Re g) | E))) by A5, Th7 .= (Integral (M,(Re (f | E)))) + (Integral (M,(Re (g | E)))) by Th7 ; then A31: R = R1 + R2 by SUPINF_2:1; dom f = dom (Im f) by COMSEQ_3:def_4; then Integral (M,(Im (f + g))) = (Integral (M,(Im (f | E)))) + (Integral (M,((Im g) | E))) by A4, A12, A30, A23, A14, A15, Th7; then R_EAL I = (R_EAL I1) + (R_EAL I2) by Th7; then I = I1 + I2 by SUPINF_2:1; then Integral (M,(f + g)) = (R1 + (I1 * )) + (R2 + (I2 * )) by A31, A22; then Integral (M,(f + g)) = (Integral (M,(f | E))) + (R2 + (I2 * )) by A6, Def3; then Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) by A24, Def3; hence ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A4, A12, A30; ::_thesis: verum end; theorem :: MESFUN6C:37 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 that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) R_EAL g is_integrable_on M by A2, MESFUNC6:def_4; then (- 1) (#) (R_EAL g) is_integrable_on M by MESFUNC5:110; then - (R_EAL g) is_integrable_on M by MESFUNC2:9; then A3: R_EAL (- g) is_integrable_on M by MESFUNC6:28; R_EAL f is_integrable_on M by A1, MESFUNC6:def_4; then consider E being Element of S such that A4: E = (dom (R_EAL f)) /\ (dom (R_EAL (- g))) and A5: Integral (M,((R_EAL f) + (R_EAL (- g)))) = (Integral (M,((R_EAL f) | E))) + (Integral (M,((R_EAL (- g)) | E))) by A3, MESFUNC5:109; take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) dom (R_EAL (- g)) = dom (- (R_EAL g)) by MESFUNC6:28; hence ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) by A4, A5, MESFUNC1:def_7, MESFUNC6:23; ::_thesis: verum end; theorem Th38: :: MESFUN6C:38 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,COMPLEX for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = 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,COMPLEX for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) let f be PartFunc of X,COMPLEX; ::_thesis: for r being Real st f is_integrable_on M holds ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = 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 * (Integral (M,f)) ) ) A1: Integral (M,(r (#) (Re f))) = Integral (M,(Re (r (#) f))) by Th2; A2: Integral (M,(r (#) (Im f))) = Integral (M,(Im (r (#) f))) by Th2; assume A3: f is_integrable_on M ; ::_thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) then A4: Re f is_integrable_on M by Def2; then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90; r (#) (Re f) is_integrable_on M by A4, MESFUNC6:102; then A6: Re (r (#) f) is_integrable_on M by Th2; then A7: Integral (M,(Re (r (#) f))) < +infty by MESFUNC6:90; A8: Im f is_integrable_on M by A3, Def2; then A9: -infty < Integral (M,(Im f)) by MESFUNC6:90; A10: Integral (M,(Im f)) < +infty by A8, MESFUNC6:90; -infty < Integral (M,(Re f)) by A4, MESFUNC6:90; then reconsider R1 = Integral (M,(Re f)), I1 = Integral (M,(Im f)) as Real by A5, A9, A10, XXREAL_0:14; A11: (R_EAL r) * (R_EAL R1) = r * R1 by Th1; A12: (R_EAL r) * (R_EAL I1) = r * I1 by Th1; r (#) (Im f) is_integrable_on M by A8, MESFUNC6:102; then A13: Im (r (#) f) is_integrable_on M by Th2; then A14: -infty < Integral (M,(Im (r (#) f))) by MESFUNC6:90; A15: Integral (M,(Im (r (#) f))) < +infty by A13, MESFUNC6:90; -infty < Integral (M,(Re (r (#) f))) by A6, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (r (#) f))), I2 = Integral (M,(Im (r (#) f))) as Real by A7, A14, A15, XXREAL_0:14; A16: Integral (M,(r (#) (Im f))) = (R_EAL r) * (Integral (M,(Im f))) by A8, MESFUNC6:102; A17: r (#) f is_integrable_on M by A6, A13, Def2; Integral (M,(r (#) (Re f))) = (R_EAL r) * (Integral (M,(Re f))) by A4, MESFUNC6:102; then R2 + (I2 * ) = r * (R1 + (I1 * )) by A16, A1, A2, A11, A12; then Integral (M,(r (#) f)) = r * (R1 + (I1 * )) by A17, Def3; hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) by A3, A6, A13, Def2, Def3; ::_thesis: verum end; theorem Th39: :: MESFUN6C:39 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,COMPLEX st f is_integrable_on M holds ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (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,COMPLEX st f is_integrable_on M holds ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (Integral (M,f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (Integral (M,f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (Integral (M,f)) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (Integral (M,f)) ) ) A1: Re ( (#) f) = - (Im f) by Th4; assume A2: f is_integrable_on M ; ::_thesis: ( (#) f is_integrable_on M & Integral (M,( (#) f)) = * (Integral (M,f)) ) then A3: Im f is_integrable_on M by Def2; A4: Im ( (#) f) = Re f by Th4; then A5: Im ( (#) f) is_integrable_on M by A2, Def2; - (Im f) = (- 1) (#) (Im f) ; then Re ( (#) f) is_integrable_on M by A3, A1, MESFUNC6:102; hence (#) f is_integrable_on M by A5, Def2; ::_thesis: Integral (M,( (#) f)) = * (Integral (M,f)) then consider R1, I1 being Real such that A6: R1 = Integral (M,(Re ( (#) f))) and A7: I1 = Integral (M,(Im ( (#) f))) and A8: Integral (M,( (#) f)) = R1 + (I1 * ) by Def3; consider R, I being Real such that A9: R = Integral (M,(Re f)) and A10: I = Integral (M,(Im f)) and A11: Integral (M,f) = R + (I * ) by A2, Def3; R1 = (R_EAL (- 1)) * (R_EAL I) by A3, A1, A10, A6, MESFUNC6:102 .= (- 1) * I by EXTREAL1:5 ; hence Integral (M,( (#) f)) = * (Integral (M,f)) by A4, A9, A11, A7, A8; ::_thesis: verum end; theorem Th40: :: MESFUN6C:40 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,COMPLEX for c being complex number st f is_integrable_on M holds ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (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,COMPLEX for c being complex number st f is_integrable_on M holds ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX for c being complex number st f is_integrable_on M holds ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX for c being complex number st f is_integrable_on M holds ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number st f is_integrable_on M holds ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) let c be complex number ; ::_thesis: ( f is_integrable_on M implies ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) ) A1: c = (Re c) + ((Im c) * ) by COMPLEX1:13; A2: dom ( (#) f) = dom f by VALUED_1:def_5; assume A3: f is_integrable_on M ; ::_thesis: ( c (#) f is_integrable_on M & Integral (M,(c (#) f)) = c * (Integral (M,f)) ) then A4: Integral (M,((Re c) (#) f)) = (Re c) * (Integral (M,f)) by Th38; A5: (#) f is_integrable_on M by A3, Th39; then A6: (Im c) (#) ( (#) f) is_integrable_on M by Th38; A7: (Re c) (#) f is_integrable_on M by A3, Th38; then consider E being Element of S such that A8: E = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) ( (#) f))) and A9: Integral (M,(((Re c) (#) f) + ((Im c) (#) ( (#) f)))) = (Integral (M,(((Re c) (#) f) | E))) + (Integral (M,(((Im c) (#) ( (#) f)) | E))) by A6, Th36; A10: dom (c (#) f) = dom f by VALUED_1:def_5; A11: Integral (M,((Im c) (#) ( (#) f))) = (Im c) * (Integral (M,( (#) f))) by A5, Th38; A12: dom ((Re c) (#) f) = dom f by VALUED_1:def_5; A13: dom ((Im c) (#) ( (#) f)) = dom ( (#) f) by VALUED_1:def_5; A14: dom (((Re c) (#) f) + ((Im c) (#) ( (#) f))) = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) ( (#) f))) by VALUED_1:def_1; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(c_(#)_f)_holds_ (c_(#)_f)_._x_=_(((Re_c)_(#)_f)_+_((Im_c)_(#)_(_(#)_f)))_._x let x be Element of X; ::_thesis: ( x in dom (c (#) f) implies (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) ( (#) f))) . x ) assume A15: x in dom (c (#) f) ; ::_thesis: (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) ( (#) f))) . x then A16: (c (#) f) . x = c * (f . x) by VALUED_1:def_5; A17: ((Im c) (#) ( (#) f)) . x = (Im c) * (( (#) f) . x) by A10, A2, A13, A15, VALUED_1:def_5; A18: ((Re c) (#) f) . x = (Re c) * (f . x) by A10, A12, A15, VALUED_1:def_5; A19: ( (#) f) . x = * (f . x) by A10, A2, A15, VALUED_1:def_5; (((Re c) (#) f) + ((Im c) (#) ( (#) f))) . x = (((Re c) (#) f) . x) + (((Im c) (#) ( (#) f)) . x) by A10, A12, A2, A13, A14, A15, VALUED_1:def_1; hence (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) ( (#) f))) . x by A1, A16, A18, A17, A19; ::_thesis: verum end; then A20: c (#) f = ((Re c) (#) f) + ((Im c) (#) ( (#) f)) by A10, A12, A2, A13, A14, PARTFUN1:5; hence c (#) f is_integrable_on M by A7, A6, Th33; ::_thesis: Integral (M,(c (#) f)) = c * (Integral (M,f)) A21: Integral (M,( (#) f)) = * (Integral (M,f)) by A3, Th39; ((Re c) (#) f) | E = (Re c) (#) f by A12, A2, A13, A8, RELAT_1:68; hence Integral (M,(c (#) f)) = ((Re c) * (Integral (M,f))) + (((Im c) * ) * (Integral (M,f))) by A12, A2, A13, A20, A4, A21, A11, A8, A9, RELAT_1:68 .= c * (Integral (M,f)) by A1 ; ::_thesis: verum end; Lm2: 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds |.(Integral (M,f)).| <= 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) = 0 implies |.(Integral (M,f)).| <= 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_integrable_on M and A3: Integral (M,f) = 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|) A4: |.f.| is_integrable_on M by A1, A2, Th31; consider R, I being Real such that A5: R = Integral (M,(Re f)) and I = Integral (M,(Im f)) and A6: Integral (M,f) = R + (I * ) by A2, Def3; R = 0 by A3, A6, COMPLEX1:4, COMPLEX1:12; then A7: |.(Integral (M,(Re f))).| = 0 by A5, EXTREAL2:5; Re f is_integrable_on M by A2, Def2; then A8: |.(Integral (M,(Re f))).| <= Integral (M,|.(Re f).|) by MESFUNC6:95; A9: dom |.f.| = dom f by VALUED_1:def_11; consider A being Element of S such that A10: A = dom f and A11: f is_measurable_on A by A1; A12: dom (Re f) = A by A10, COMSEQ_3:def_3; A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(Re_f)_holds_ |.((Re_f)_._x).|_<=_|.f.|_._x let x be Element of X; ::_thesis: ( x in dom (Re f) implies |.((Re f) . x).| <= |.f.| . x ) assume A14: x in dom (Re f) ; ::_thesis: |.((Re f) . x).| <= |.f.| . x then A15: (Re f) . x = Re (f . x) by COMSEQ_3:def_3; |.f.| . x = |.(f . x).| by A10, A12, A9, A14, VALUED_1:def_11; hence |.((Re f) . x).| <= |.f.| . x by A15, COMPLEX1:79; ::_thesis: verum end; Re f is_measurable_on A by A11, Def1; hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A3, A4, A8, A10, A12, A9, A13, A7, COMPLEX1:44, MESFUNC6:96; ::_thesis: verum end; theorem Th41: :: MESFUN6C:41 for X being non empty set for f being PartFunc of X,REAL for Y being set for r being Real holds (r (#) f) | Y = r (#) (f | Y) proof let X be non empty set ; ::_thesis: for f being PartFunc of X,REAL for Y being set for r being Real holds (r (#) f) | Y = r (#) (f | Y) let f be PartFunc of X,REAL; ::_thesis: for Y being set for r being Real holds (r (#) f) | Y = r (#) (f | Y) let Y be set ; ::_thesis: for r being Real holds (r (#) f) | Y = r (#) (f | Y) let r be Real; ::_thesis: (r (#) f) | Y = r (#) (f | Y) A1: dom ((r (#) f) | Y) = (dom (r (#) f)) /\ Y by RELAT_1:61 .= (dom f) /\ Y by VALUED_1:def_5 .= dom (f | Y) by RELAT_1:61 ; A2: dom ((r (#) f) | Y) c= dom (r (#) f) by RELAT_1:60; A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((r_(#)_f)_|_Y)_holds_ (r_(#)_(f_|_Y))_._x_=_((r_(#)_f)_|_Y)_._x let x be Element of X; ::_thesis: ( x in dom ((r (#) f) | Y) implies (r (#) (f | Y)) . x = ((r (#) f) | Y) . x ) assume A4: x in dom ((r (#) f) | Y) ; ::_thesis: (r (#) (f | Y)) . x = ((r (#) f) | Y) . x then x in dom (r (#) (f | Y)) by A1, VALUED_1:def_5; then (r (#) (f | Y)) . x = r * ((f | Y) . x) by VALUED_1:def_5; then (r (#) (f | Y)) . x = r * (f . x) by A1, A4, FUNCT_1:47; then (r (#) (f | Y)) . x = (r (#) f) . x by A2, A4, VALUED_1:def_5; hence (r (#) (f | Y)) . x = ((r (#) f) | Y) . x by A4, FUNCT_1:47; ::_thesis: verum end; dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by A1, VALUED_1:def_5; hence (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; ::_thesis: verum end; theorem Th42: :: MESFUN6C:42 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) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,REAL st ex A being Element of S st ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st ex A being Element of S st ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex A being Element of S st ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) let f, g be PartFunc of X,REAL; ::_thesis: ( ex A being Element of S st ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) & f is_integrable_on M & g is_integrable_on M & g - f is nonnegative implies ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) ) assume that A1: ex A being Element of S st ( A = (dom f) /\ (dom g) & f is_measurable_on A & g is_measurable_on A ) and A2: f is_integrable_on M and A3: g is_integrable_on M and A4: g - f is nonnegative ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) set h = (- 1) (#) f; (- 1) (#) f is_integrable_on M by A2, MESFUNC6:102; then consider E being Element of S such that A5: E = (dom ((- 1) (#) f)) /\ (dom g) and A6: Integral (M,(((- 1) (#) f) + g)) = (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A3, MESFUNC6:101; A7: f | E is_integrable_on M by A2, MESFUNC6:91; then A8: Integral (M,(f | E)) < +infty by MESFUNC6:90; -infty < Integral (M,(f | E)) by A7, MESFUNC6:90; then reconsider c1 = Integral (M,(f | E)) as Real by A8, XXREAL_0:14; A9: (R_EAL (- 1)) * (Integral (M,(f | E))) = (- 1) * c1 by EXTREAL1:1; A10: g | E is_integrable_on M by A3, MESFUNC6:91; then A11: Integral (M,(g | E)) < +infty by MESFUNC6:90; -infty < Integral (M,(g | E)) by A10, MESFUNC6:90; then reconsider c2 = Integral (M,(g | E)) as Real by A11, XXREAL_0:14; take E ; ::_thesis: ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) A12: ((- 1) (#) f) | E = (- 1) (#) (f | E) by Th41; consider A being Element of S such that A13: A = (dom f) /\ (dom g) and A14: f is_measurable_on A and A15: g is_measurable_on A by A1; dom ((- 1) (#) f) = dom f by VALUED_1:def_5; then A16: dom (((- 1) (#) f) + g) = A by A13, VALUED_1:def_1; (- 1) (#) f is_measurable_on A by A13, A14, MESFUNC6:21, XBOOLE_1:17; then 0 <= (Integral (M,(((- 1) (#) f) | E))) + (Integral (M,(g | E))) by A4, A6, A15, A16, MESFUNC6:26, MESFUNC6:84; then 0 <= ((R_EAL (- 1)) * (Integral (M,(f | E)))) + (Integral (M,(g | E))) by A7, A12, MESFUNC6:102; then 0 <= (- c1) + c2 by A9, SUPINF_2:1; then 0 + c1 <= ((- c1) + c2) + c1 by XREAL_1:6; hence ( E = (dom f) /\ (dom g) & Integral (M,(f | E)) <= Integral (M,(g | E)) ) by A5, VALUED_1:def_5; ::_thesis: verum end; Lm3: 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds |.(Integral (M,f)).| <= 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M & Integral (M,f) <> 0 implies |.(Integral (M,f)).| <= 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_integrable_on M and A3: Integral (M,f) <> 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|) A4: |.f.| is_integrable_on M by A1, A2, Th31; set a = Integral (M,f); 0 < |.(Integral (M,f)).| by A3, COMPLEX1:47; then A5: |.(Integral (M,f)).| / |.(Integral (M,f)).| = 1 by XCMPLX_1:60; set h = f (#) (|.f.| "); set b = (Integral (M,f)) / |.(Integral (M,f)).|; A6: dom |.f.| = dom f by VALUED_1:def_11; |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *')).| by COMPLEX1:65; then |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by COMPLEX1:69; then A7: |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| = |.((Integral (M,f)) / |.(Integral (M,f)).|).| * |.((Integral (M,f)) / |.(Integral (M,f)).|).| by COMPLEX1:65; A8: f (#) (|.f.| ") = f /" |.f.| ; then A9: dom (f (#) (|.f.| ")) = (dom f) /\ (dom |.f.|) by VALUED_1:16; then A10: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) = dom f by A6, VALUED_1:def_5; then A11: dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) = (dom f) /\ (dom f) by A6, VALUED_1:def_4; then A12: dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = dom f by COMSEQ_3:def_3; A13: dom (|.f.| (#) (f (#) (|.f.| "))) = (dom |.f.|) /\ (dom (f (#) (|.f.| "))) by VALUED_1:def_4; then A14: dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) = dom f by A6, A9, VALUED_1:def_5; now__::_thesis:_for_x_being_set_st_x_in_dom_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(|.f.|_(#)_(f_(#)_(|.f.|_"))))_holds_ ((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(|.f.|_(#)_(f_(#)_(|.f.|_"))))_._x_=_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_"))))_._x let x be set ; ::_thesis: ( x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) implies ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x ) assume A15: x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) ; ::_thesis: ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x then x in dom (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) by A6, A9, A13, A11, VALUED_1:def_5; then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by VALUED_1:def_4; then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A14, A15, VALUED_1:def_11; then A16: (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x)) * |.(f . x).| by A14, A10, A15, VALUED_1:def_5; ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| (#) (f (#) (|.f.| "))) . x) by A15, VALUED_1:def_5; then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((|.f.| . x) * ((f (#) (|.f.| ")) . x)) by A6, A9, A13, A14, A15, VALUED_1:def_4; then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (|.(f . x).| * ((f (#) (|.f.| ")) . x)) by A6, A14, A15, VALUED_1:def_11; hence ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| ")))) . x = (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x by A16; ::_thesis: verum end; then A17: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) = |.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A14, A11, FUNCT_1:2; A18: |.((Integral (M,f)) / |.(Integral (M,f)).|).| = |.(Integral (M,f)).| / |.|.(Integral (M,f)).|.| by COMPLEX1:67; now__::_thesis:_for_x_being_set_st_x_in_(dom_(Re_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_"))))))_/\_(dom_|.f.|)_holds_ (Re_(|.f.|_(#)_((((Integral_(M,f))_/_|.(Integral_(M,f)).|)_*')_(#)_(f_(#)_(|.f.|_")))))_._x_<=_|.f.|_._x let x be set ; ::_thesis: ( x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) implies (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 ) A19: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17; assume A20: x in (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 then |.f.| . x = |.(f . x).| by A6, A12, VALUED_1:def_11; then A21: |.((f (#) (|.f.| ")) . x).| = |.(f . x).| / |.|.(f . x).|.| by A19, COMPLEX1:67; percases ( f . x <> 0 or f . x = 0 ) ; supposeA22: f . x <> 0 ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 A23: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def_3; (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def_4; then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def_11; then A24: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65; x in dom ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) by A9, A12, A20, VALUED_1:def_5; then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x = (((Integral (M,f)) / |.(Integral (M,f)).|) *') * ((f (#) (|.f.| ")) . x) by VALUED_1:def_5; then A25: |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| = |.(((Integral (M,f)) / |.(Integral (M,f)).|) *').| * |.((f (#) (|.f.| ")) . x).| by COMPLEX1:65; 0 < |.(f . x).| by A22, COMPLEX1:47; then |.(f . x).| / |.(f . x).| = 1 by XCMPLX_1:60; then Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A7, A18, A5, A21, A25, A24, COMPLEX1:54; hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A23, VALUED_1:def_11; ::_thesis: verum end; supposeA26: f . x = 0 ; ::_thesis: (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . b1 <= |.f.| . b1 (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = (|.f.| . x) * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A11, A12, A20, VALUED_1:def_4; then (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x = |.(f . x).| * (((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x) by A6, A12, A20, VALUED_1:def_11; then A27: |.((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x).| = |.|.(f . x).|.| * |.(((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))) . x).| by COMPLEX1:65; ((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by A26, COMPLEX1:5; then A28: Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) <= |.(f . x).| by A27, COMPLEX1:54, SQUARE_1:17; Re ((|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) . x) = (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x by A6, A12, A20, COMSEQ_3:def_3; hence (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) . x <= |.f.| . x by A6, A12, A20, A28, VALUED_1:def_11; ::_thesis: verum end; end; end; then A29: |.f.| - (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) is nonnegative by MESFUNC6:58; set F = Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))); reconsider b1 = (Integral (M,f)) / |.(Integral (M,f)).| as Element of COMPLEX ; A30: Re (b1 * (b1 *')) = ((Re b1) ^2) + ((Im b1) ^2) by COMPLEX1:40; consider A being Element of S such that A31: A = dom f and A32: f is_measurable_on A by A1; A33: |.f.| is_measurable_on A by A31, A32, Th30; A34: now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(|.f.|_(#)_(f_(#)_(|.f.|_")))_._x let x be set ; ::_thesis: ( x in dom f implies f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 ) A35: (f (#) (|.f.| ")) . x = (f . x) / (|.f.| . x) by A8, VALUED_1:17; assume A36: x in dom f ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 then A37: |.f.| . x = |.(f . x).| by A6, VALUED_1:def_11; A38: (|.f.| (#) (f (#) (|.f.| "))) . x = (|.f.| . x) * ((f (#) (|.f.| ")) . x) by A6, A9, A13, A36, VALUED_1:def_4; percases ( f . x <> 0 or f . x = 0 ) ; suppose f . x <> 0 ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 then 0 < |.(f . x).| by COMPLEX1:47; hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A38, A37, A35, XCMPLX_1:87; ::_thesis: verum end; supposeA39: f . x = 0 ; ::_thesis: f . b1 = (|.f.| (#) (f (#) (|.f.| "))) . b1 then ((Re (f . x)) ^2) + ((Im (f . x)) ^2) = 0 by COMPLEX1:5; then f . x = ((f (#) (|.f.| ")) . x) * |.(f . x).| by A39, SQUARE_1:17; hence f . x = (|.f.| (#) (f (#) (|.f.| "))) . x by A6, A36, A38, VALUED_1:def_11; ::_thesis: verum end; end; end; then A40: f = |.f.| (#) (f (#) (|.f.| ")) by A6, A9, A13, FUNCT_1:2; then A41: (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is_integrable_on M by A2, Th40; then consider R1, I1 being Real such that A42: R1 = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and I1 = Integral (M,(Im (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) and A43: Integral (M,(|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) = R1 + (I1 * ) by A17, Def3; A44: Im (b1 * (b1 *')) = 0 by COMPLEX1:40; ((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = (Re (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) + ((Im (((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *'))) * ) by COMPLEX1:13; then ((Integral (M,f)) / |.(Integral (M,f)).|) * (((Integral (M,f)) / |.(Integral (M,f)).|) *') = |.(((Integral (M,f)) / |.(Integral (M,f)).|) * ((Integral (M,f)) / |.(Integral (M,f)).|)).| by A30, A44, COMPLEX1:68; then ((((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f))) / |.(Integral (M,f)).| = 1 by A7, A18, A5, COMPLEX1:65; then A45: (((Integral (M,f)) / |.(Integral (M,f)).|) *') * (Integral (M,f)) = |.(Integral (M,f)).| by XCMPLX_1:58; Re (R1 + (I1 * )) = R1 by COMPLEX1:12; then Re |.(Integral (M,f)).| = R1 by A2, A45, A40, A17, A43, Th40; then A46: |.(Integral (M,f)).| = Integral (M,(Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) by A42, COMPLEX1:def_1; |.f.| (#) (f (#) (|.f.| ")) is_measurable_on A by A32, A6, A9, A13, A34, FUNCT_1:2; then (((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (|.f.| (#) (f (#) (|.f.| "))) is_measurable_on A by A31, A6, A9, A13, Th17; then A47: Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is_measurable_on A by A17, Def1; Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))) is_integrable_on M by A17, A41, Def2; then consider E being Element of S such that A48: E = (dom (Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| ")))))) /\ (dom |.f.|) and A49: Integral (M,((Re (|.f.| (#) ((((Integral (M,f)) / |.(Integral (M,f)).|) *') (#) (f (#) (|.f.| "))))) | E)) <= Integral (M,(|.f.| | E)) by A4, A31, A6, A33, A47, A12, A29, Th42; |.f.| | E = |.f.| by A6, A12, A48, RELAT_1:68; hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A6, A46, A12, A48, A49, RELAT_1:68; ::_thesis: verum end; theorem :: MESFUN6C:43 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds |.(Integral (M,f)).| <= 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,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M holds |.(Integral (M,f)).| <= Integral (M,|.f.|) let f be PartFunc of X,COMPLEX; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & f is_integrable_on M implies |.(Integral (M,f)).| <= 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_integrable_on M ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|) percases ( Integral (M,f) = 0 or Integral (M,f) <> 0 ) ; suppose Integral (M,f) = 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|) hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A1, A2, Lm2; ::_thesis: verum end; suppose Integral (M,f) <> 0 ; ::_thesis: |.(Integral (M,f)).| <= Integral (M,|.f.|) hence |.(Integral (M,f)).| <= Integral (M,|.f.|) by A1, A2, Lm3; ::_thesis: verum end; end; 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,COMPLEX; let B be Element of S; func Integral_on (M,B,f) -> complex number equals :: MESFUN6C:def 5 Integral (M,(f | B)); coherence Integral (M,(f | B)) is complex number ; end; :: deftheorem defines Integral_on MESFUN6C: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,COMPLEX for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B)); theorem :: MESFUN6C:44 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; ::_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 and A2: g is_integrable_on M and A3: 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)) ) A4: Re f is_integrable_on M by A1, Def2; then (Re f) | B is_integrable_on M by MESFUNC6:91; then A5: Re (f | B) is_integrable_on M by Th7; then A6: Integral (M,(Re (f | B))) < +infty by MESFUNC6:90; A7: Im f is_integrable_on M by A1, Def2; then (Im f) | B is_integrable_on M by MESFUNC6:91; then A8: Im (f | B) is_integrable_on M by Th7; then A9: -infty < Integral (M,(Im (f | B))) by MESFUNC6:90; A10: Integral (M,(Im (f | B))) < +infty by A8, MESFUNC6:90; -infty < Integral (M,(Re (f | B))) by A5, MESFUNC6:90; then reconsider R1 = Integral (M,(Re (f | B))), I1 = Integral (M,(Im (f | B))) as Real by A6, A9, A10, XXREAL_0:14; f | B is_integrable_on M by A5, A8, Def2; then A11: Integral (M,(f | B)) = R1 + (I1 * ) by Def3; A12: Im g is_integrable_on M by A2, Def2; then (Im g) | B is_integrable_on M by MESFUNC6:91; then A13: Im (g | B) is_integrable_on M by Th7; then A14: -infty < Integral (M,(Im (g | B))) by MESFUNC6:90; A15: Re g is_integrable_on M by A2, Def2; then (Re g) | B is_integrable_on M by MESFUNC6:91; then A16: Re (g | B) is_integrable_on M by Th7; then A17: Integral (M,(Re (g | B))) < +infty by MESFUNC6:90; B c= dom (Im (f + g)) by A3, COMSEQ_3:def_4; then A18: B c= dom ((Im f) + (Im g)) by Th5; then Integral_on (M,B,((Im f) + (Im g))) = (Integral_on (M,B,(Im f))) + (Integral_on (M,B,(Im g))) by A7, A12, MESFUNC6:103; then A19: Integral (M,((Im (f + g)) | B)) = (Integral (M,((Im f) | B))) + (Integral (M,((Im g) | B))) by Th5; A20: Integral (M,(Im (g | B))) < +infty by A13, MESFUNC6:90; -infty < Integral (M,(Re (g | B))) by A16, MESFUNC6:90; then reconsider R2 = Integral (M,(Re (g | B))), I2 = Integral (M,(Im (g | B))) as Real by A17, A14, A20, XXREAL_0:14; g | B is_integrable_on M by A16, A13, Def2; then A21: Integral (M,(g | B)) = R2 + (I2 * ) by Def3; A22: Integral (M,((Im g) | B)) = I2 by Th7; (Im f) + (Im g) is_integrable_on M by A7, A12, A18, MESFUNC6:103; then A23: Im (f + g) is_integrable_on M by Th5; then (Im (f + g)) | B is_integrable_on M by MESFUNC6:91; then A24: Im ((f + g) | B) is_integrable_on M by Th7; then A25: -infty < Integral (M,(Im ((f + g) | B))) by MESFUNC6:90; B c= dom (Re (f + g)) by A3, COMSEQ_3:def_3; then A26: B c= dom ((Re f) + (Re g)) by Th5; then Integral_on (M,B,((Re f) + (Re g))) = (Integral_on (M,B,(Re f))) + (Integral_on (M,B,(Re g))) by A4, A15, MESFUNC6:103; then A27: Integral (M,((Re (f + g)) | B)) = (Integral (M,((Re f) | B))) + (Integral (M,((Re g) | B))) by Th5; (Re f) + (Re g) is_integrable_on M by A4, A15, A26, MESFUNC6:103; then A28: Re (f + g) is_integrable_on M by Th5; then (Re (f + g)) | B is_integrable_on M by MESFUNC6:91; then A29: Re ((f + g) | B) is_integrable_on M by Th7; then A30: Integral (M,(Re ((f + g) | B))) < +infty by MESFUNC6:90; A31: Integral (M,(Im ((f + g) | B))) < +infty by A24, MESFUNC6:90; -infty < Integral (M,(Re ((f + g) | B))) by A29, MESFUNC6:90; then reconsider R = Integral (M,(Re ((f + g) | B))), I = Integral (M,(Im ((f + g) | B))) as Real by A30, A25, A31, XXREAL_0:14; A32: Integral (M,((Re g) | B)) = R2 by Th7; Integral (M,((Im f) | B)) = I1 by Th7; then R_EAL I = (R_EAL I1) + (R_EAL I2) by A19, A22, Th7; then A33: I = I1 + I2 by SUPINF_2:1; Integral (M,((Re f) | B)) = R1 by Th7; then R_EAL R = (R_EAL R1) + (R_EAL R2) by A27, A32, Th7; then A34: R = R1 + R2 by SUPINF_2:1; (f + g) | B is_integrable_on M by A29, A24, Def2; then Integral_on (M,B,(f + g)) = R + (I * ) by Def3 .= (Integral_on (M,B,f)) + (Integral_on (M,B,g)) by A34, A33, A11, A21 ; hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A28, A23, Def2; ::_thesis: verum end; theorem :: MESFUN6C:45 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,COMPLEX for c being complex number for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (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,COMPLEX for c being complex number for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (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,COMPLEX for c being complex number for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX for c being complex number for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) let f be PartFunc of X,COMPLEX; ::_thesis: for c being complex number for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) let c be complex number ; ::_thesis: for B being Element of S st f is_integrable_on M holds Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) let B be Element of S; ::_thesis: ( f is_integrable_on M implies Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) ) assume f is_integrable_on M ; ::_thesis: Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) then A1: f | B is_integrable_on M by Th23; A2: dom ((c (#) f) | B) = (dom (c (#) f)) /\ B by RELAT_1:61; then dom ((c (#) f) | B) = (dom f) /\ B by VALUED_1:def_5; then A3: dom ((c (#) f) | B) = dom (f | B) by RELAT_1:61; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_((c_(#)_f)_|_B)_holds_ ((c_(#)_f)_|_B)_._x_=_(c_(#)_(f_|_B))_._x let x be set ; ::_thesis: ( x in dom ((c (#) f) | B) implies ((c (#) f) | B) . x = (c (#) (f | B)) . x ) assume A5: x in dom ((c (#) f) | B) ; ::_thesis: ((c (#) f) | B) . x = (c (#) (f | B)) . x then A6: ((c (#) f) | B) . x = (c (#) f) . x by FUNCT_1:47; x in dom (c (#) f) by A2, A5, XBOOLE_0:def_4; then ((c (#) f) | B) . x = c * (f . x) by A6, VALUED_1:def_5; then A7: ((c (#) f) | B) . x = c * ((f | B) . x) by A3, A5, FUNCT_1:47; x in dom (c (#) (f | B)) by A3, A5, VALUED_1:def_5; hence ((c (#) f) | B) . x = (c (#) (f | B)) . x by A7, VALUED_1:def_5; ::_thesis: verum end; dom ((c (#) f) | B) = dom (c (#) (f | B)) by A3, VALUED_1:def_5; then (c (#) f) | B = c (#) (f | B) by A4, FUNCT_1:2; hence Integral_on (M,B,(c (#) f)) = c * (Integral_on (M,B,f)) by A1, Th40; ::_thesis: verum end; begin theorem :: MESFUN6C:46 for X being non empty set for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let S be SigmaField of X; ::_thesis: for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let A be Element of S; ::_thesis: for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let a be Real; ::_thesis: ( A c= dom f implies A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) ) now__::_thesis:_for_x_being_set_st_x_in_A_/\_(great_eq_dom_(f,a))_holds_ x_in_A_\_(A_/\_(less_dom_(f,a))) let x be set ; ::_thesis: ( x in A /\ (great_eq_dom (f,a)) implies x in A \ (A /\ (less_dom (f,a))) ) assume A1: x in A /\ (great_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_dom (f,a))) then x in great_eq_dom (f,a) by XBOOLE_0:def_4; then ex y being Real st ( y = f . x & a <= y ) by MESFUNC6:6; then for y1 being Real holds ( not y1 = f . x or not y1 < a ) ; then not x in less_dom (f,a) by MESFUNC6:3; then A2: not x in A /\ (less_dom (f,a)) by XBOOLE_0:def_4; x in A by A1, XBOOLE_0:def_4; hence x in A \ (A /\ (less_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum end; then A3: A /\ (great_eq_dom (f,a)) c= A \ (A /\ (less_dom (f,a))) by TARSKI:def_3; assume A4: A c= dom f ; ::_thesis: A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(less_dom_(f,a)))_holds_ x_in_A_/\_(great_eq_dom_(f,a)) let x be set ; ::_thesis: ( x in A \ (A /\ (less_dom (f,a))) implies x in A /\ (great_eq_dom (f,a)) ) assume A5: x in A \ (A /\ (less_dom (f,a))) ; ::_thesis: x in A /\ (great_eq_dom (f,a)) then A6: x in A by XBOOLE_0:def_5; not x in A /\ (less_dom (f,a)) by A5, XBOOLE_0:def_5; then not x in less_dom (f,a) by A6, XBOOLE_0:def_4; then not f . x < a by A4, A6, MESFUNC6:3; then x in great_eq_dom (f,a) by A4, A6, MESFUNC6:6; hence x in A /\ (great_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (less_dom (f,a))) c= A /\ (great_eq_dom (f,a)) by TARSKI:def_3; hence A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUN6C:47 for X being non empty set for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let S be SigmaField of X; ::_thesis: for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let A be Element of S; ::_thesis: for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let a be Real; ::_thesis: ( A c= dom f implies A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) ) now__::_thesis:_for_x_being_set_st_x_in_A_/\_(great_dom_(f,a))_holds_ x_in_A_\_(A_/\_(less_eq_dom_(f,a))) let x be set ; ::_thesis: ( x in A /\ (great_dom (f,a)) implies x in A \ (A /\ (less_eq_dom (f,a))) ) assume A1: x in A /\ (great_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_eq_dom (f,a))) then x in great_dom (f,a) by XBOOLE_0:def_4; then ex y being Real st ( y = f . x & a < y ) by MESFUNC6:5; then for y1 being Real holds ( not y1 = f . x or not y1 <= a ) ; then not x in less_eq_dom (f,a) by MESFUNC6:4; then A2: not x in A /\ (less_eq_dom (f,a)) by XBOOLE_0:def_4; x in A by A1, XBOOLE_0:def_4; hence x in A \ (A /\ (less_eq_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum end; then A3: A /\ (great_dom (f,a)) c= A \ (A /\ (less_eq_dom (f,a))) by TARSKI:def_3; assume A4: A c= dom f ; ::_thesis: A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(less_eq_dom_(f,a)))_holds_ x_in_A_/\_(great_dom_(f,a)) let x be set ; ::_thesis: ( x in A \ (A /\ (less_eq_dom (f,a))) implies x in A /\ (great_dom (f,a)) ) assume A5: x in A \ (A /\ (less_eq_dom (f,a))) ; ::_thesis: x in A /\ (great_dom (f,a)) then A6: x in A by XBOOLE_0:def_5; not x in A /\ (less_eq_dom (f,a)) by A5, XBOOLE_0:def_5; then not x in less_eq_dom (f,a) by A6, XBOOLE_0:def_4; then not f . x <= a by A4, A6, MESFUNC6:4; then x in great_dom (f,a) by A4, A6, MESFUNC6:5; hence x in A /\ (great_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (less_eq_dom (f,a))) c= A /\ (great_dom (f,a)) by TARSKI:def_3; hence A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUN6C:48 for X being non empty set for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let S be SigmaField of X; ::_thesis: for A being Element of S for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let A be Element of S; ::_thesis: for f being PartFunc of X,REAL for a being Real st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let f be PartFunc of X,REAL; ::_thesis: for a being Real st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let a be Real; ::_thesis: ( A c= dom f implies A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) ) now__::_thesis:_for_x_being_set_st_x_in_A_/\_(less_eq_dom_(f,a))_holds_ x_in_A_\_(A_/\_(great_dom_(f,a))) let x be set ; ::_thesis: ( x in A /\ (less_eq_dom (f,a)) implies x in A \ (A /\ (great_dom (f,a))) ) assume A1: x in A /\ (less_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_dom (f,a))) then x in less_eq_dom (f,a) by XBOOLE_0:def_4; then ex y being Real st ( y = f . x & y <= a ) by MESFUNC6:4; then for y1 being Real holds ( not y1 = f . x or not a < y1 ) ; then not x in great_dom (f,a) by MESFUNC6:5; then A2: not x in A /\ (great_dom (f,a)) by XBOOLE_0:def_4; x in A by A1, XBOOLE_0:def_4; hence x in A \ (A /\ (great_dom (f,a))) by A2, XBOOLE_0:def_5; ::_thesis: verum end; then A3: A /\ (less_eq_dom (f,a)) c= A \ (A /\ (great_dom (f,a))) by TARSKI:def_3; assume A4: A c= dom f ; ::_thesis: A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) now__::_thesis:_for_x_being_set_st_x_in_A_\_(A_/\_(great_dom_(f,a)))_holds_ x_in_A_/\_(less_eq_dom_(f,a)) let x be set ; ::_thesis: ( x in A \ (A /\ (great_dom (f,a))) implies x in A /\ (less_eq_dom (f,a)) ) assume A5: x in A \ (A /\ (great_dom (f,a))) ; ::_thesis: x in A /\ (less_eq_dom (f,a)) then A6: x in A by XBOOLE_0:def_5; not x in A /\ (great_dom (f,a)) by A5, XBOOLE_0:def_5; then not x in great_dom (f,a) by A6, XBOOLE_0:def_4; then not a < f . x by A4, A6, MESFUNC6:5; then x in less_eq_dom (f,a) by A4, A6, MESFUNC6:4; hence x in A /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (great_dom (f,a))) c= A /\ (less_eq_dom (f,a)) by TARSKI:def_3; hence A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUN6C:49 for X being non empty set for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for A being Element of S for f being PartFunc of X,REAL for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let S be SigmaField of X; ::_thesis: for A being Element of S for f being PartFunc of X,REAL for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let A be Element of S; ::_thesis: for f being PartFunc of X,REAL for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let f be PartFunc of X,REAL; ::_thesis: for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let a be Real; ::_thesis: A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) now__::_thesis:_for_x_being_set_st_x_in_(A_/\_(great_eq_dom_(f,a)))_/\_(less_eq_dom_(f,a))_holds_ x_in_A_/\_(eq_dom_(f,a)) let x be set ; ::_thesis: ( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) ) assume A1: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; ::_thesis: x in A /\ (eq_dom (f,a)) then A2: x in less_eq_dom (f,a) by XBOOLE_0:def_4; then A3: x in dom f by MESFUNC6:4; A4: x in A /\ (great_eq_dom (f,a)) by A1, XBOOLE_0:def_4; then x in great_eq_dom (f,a) by XBOOLE_0:def_4; then A5: ex y1 being Real st ( y1 = f . x & a <= y1 ) by MESFUNC6:6; ex y2 being Real st ( y2 = f . x & y2 <= a ) by A2, MESFUNC6:4; then a = f . x by A5, XXREAL_0:1; then A6: x in eq_dom (f,a) by A3, MESFUNC6:7; x in A by A4, XBOOLE_0:def_4; hence x in A /\ (eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A7: (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_A_/\_(eq_dom_(f,a))_holds_ x_in_(A_/\_(great_eq_dom_(f,a)))_/\_(less_eq_dom_(f,a)) let x be set ; ::_thesis: ( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ) assume A8: x in A /\ (eq_dom (f,a)) ; ::_thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) then A9: x in A by XBOOLE_0:def_4; A10: x in eq_dom (f,a) by A8, XBOOLE_0:def_4; then A11: ex y being Real st ( y = f . x & a = y ) by MESFUNC6:7; A12: x in dom f by A10, MESFUNC6:7; then x in great_eq_dom (f,a) by A11, MESFUNC6:6; then A13: x in A /\ (great_eq_dom (f,a)) by A9, XBOOLE_0:def_4; x in less_eq_dom (f,a) by A11, A12, MESFUNC6:4; hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A13, XBOOLE_0:def_4; ::_thesis: verum end; then A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by TARSKI:def_3; hence A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A7, XBOOLE_0:def_10; ::_thesis: verum end;