:: MESFUN7C semantic presentation begin definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func R_EAL f -> Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 1 f; coherence f is Functional_Sequence of X,ExtREAL proof ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of X,ExtREAL ) ) by NUMBERS:31, RELSET_1:7, SEQFUNC:1; hence f is Functional_Sequence of X,ExtREAL by SEQFUNC:1; ::_thesis: verum end; end; :: deftheorem defines R_EAL MESFUN7C:def_1_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds R_EAL f = f; theorem Th1: :: MESFUN7C:1 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X holds f # x = (R_EAL f) # x proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X holds f # x = (R_EAL f) # x let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X holds f # x = (R_EAL f) # x let x be Element of X; ::_thesis: f # x = (R_EAL f) # x now__::_thesis:_for_r_being_set_st_r_in_rng_((R_EAL_f)_#_x)_holds_ r_in_REAL let r be set ; ::_thesis: ( r in rng ((R_EAL f) # x) implies r in REAL ) assume r in rng ((R_EAL f) # x) ; ::_thesis: r in REAL then consider n being set such that A1: n in NAT and A2: ((R_EAL f) # x) . n = r by FUNCT_2:11; reconsider n = n as Element of NAT by A1; r = ((R_EAL f) . n) . x by A2, MESFUNC5:def_13 .= (R_EAL (f . n)) . x .= (f . n) . x ; hence r in REAL ; ::_thesis: verum end; then rng ((R_EAL f) # x) c= REAL by TARSKI:def_3; then reconsider RFx = (R_EAL f) # x as Function of NAT,REAL by FUNCT_2:6; reconsider RFx = RFx as Real_Sequence ; now__::_thesis:_for_n_being_set_st_n_in_NAT_holds_ RFx_._n_=_(f_#_x)_._n let n be set ; ::_thesis: ( n in NAT implies RFx . n = (f # x) . n ) assume n in NAT ; ::_thesis: RFx . n = (f # x) . n then reconsider n1 = n as Element of NAT ; RFx . n = ((R_EAL f) . n1) . x by MESFUNC5:def_13 .= (R_EAL (f . n1)) . x ; hence RFx . n = (f # x) . n by SEQFUNC:def_10; ::_thesis: verum end; hence f # x = (R_EAL f) # x by FUNCT_2:12; ::_thesis: verum end; registration let X be non empty set ; let f be Function of X,REAL; cluster R_EAL f -> total ; coherence R_EAL f is total ; end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 2 inf (R_EAL f); coherence inf (R_EAL f) is PartFunc of X,ExtREAL ; end; :: deftheorem defines inf MESFUN7C:def_2_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds inf f = inf (R_EAL f); theorem Th2: :: MESFUN7C:2 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (inf f) holds (inf f) . x = inf (rng (R_EAL (f # x))) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (inf f) holds (inf f) . x = inf (rng (R_EAL (f # x))) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (inf f) holds (inf f) . x = inf (rng (R_EAL (f # x))) let x be Element of X; ::_thesis: ( x in dom (inf f) implies (inf f) . x = inf (rng (R_EAL (f # x))) ) assume x in dom (inf f) ; ::_thesis: (inf f) . x = inf (rng (R_EAL (f # x))) then (inf f) . x = inf ((R_EAL f) # x) by MESFUNC8:def_3; hence (inf f) . x = inf (rng (R_EAL (f # x))) by Th1; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 3 sup (R_EAL f); coherence sup (R_EAL f) is PartFunc of X,ExtREAL ; end; :: deftheorem defines sup MESFUN7C:def_3_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds sup f = sup (R_EAL f); theorem Th3: :: MESFUN7C:3 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (sup f) holds (sup f) . x = sup (rng (R_EAL (f # x))) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (sup f) holds (sup f) . x = sup (rng (R_EAL (f # x))) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (sup f) holds (sup f) . x = sup (rng (R_EAL (f # x))) let x be Element of X; ::_thesis: ( x in dom (sup f) implies (sup f) . x = sup (rng (R_EAL (f # x))) ) assume x in dom (sup f) ; ::_thesis: (sup f) . x = sup (rng (R_EAL (f # x))) then (sup f) . x = sup ((R_EAL f) # x) by MESFUNC8:def_4; hence (sup f) . x = sup (rng (R_EAL (f # x))) by Th1; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 4 inferior_realsequence (R_EAL f); coherence inferior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ; end; :: deftheorem defines inferior_realsequence MESFUN7C:def_4_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds inferior_realsequence f = inferior_realsequence (R_EAL f); theorem Th4: :: MESFUN7C:4 for X being non empty set for f being Functional_Sequence of X,REAL for n being Nat holds ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for n being Nat holds ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) ) let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) ) let n be Nat; ::_thesis: ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) ) set IF = inferior_realsequence f; dom ((inferior_realsequence f) . n) = dom ((R_EAL f) . 0) by MESFUNC8:def_5 .= dom (R_EAL (f . 0)) ; hence dom ((inferior_realsequence f) . n) = dom (f . 0) ; ::_thesis: for x being Element of X st x in dom ((inferior_realsequence f) . n) holds ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n A1: n in NAT by ORDINAL1:def_12; hereby ::_thesis: verum let x be Element of X; ::_thesis: ( x in dom ((inferior_realsequence f) . n) implies ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) assume x in dom ((inferior_realsequence f) . n) ; ::_thesis: ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n then A2: ((inferior_realsequence f) . n) . x = (inferior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_5 .= inf (((R_EAL f) # x) ^\ n) by A1, RINFSUP2:27 ; (R_EAL f) # x = f # x by Th1; hence ((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n by A1, A2, RINFSUP2:27; ::_thesis: verum end; end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 5 superior_realsequence (R_EAL f); coherence superior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ; end; :: deftheorem defines superior_realsequence MESFUN7C:def_5_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds superior_realsequence f = superior_realsequence (R_EAL f); theorem Th5: :: MESFUN7C:5 for X being non empty set for f being Functional_Sequence of X,REAL for n being Nat holds ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for n being Nat holds ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) ) let f be Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) ) let n be Nat; ::_thesis: ( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) ) set SF = superior_realsequence f; thus dom ((superior_realsequence f) . n) = dom (f . 0) by MESFUNC8:def_6; ::_thesis: for x being Element of X st x in dom ((superior_realsequence f) . n) holds ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n hereby ::_thesis: verum let x be Element of X; ::_thesis: ( x in dom ((superior_realsequence f) . n) implies ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) assume x in dom ((superior_realsequence f) . n) ; ::_thesis: ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n then ((superior_realsequence f) . n) . x = (superior_realsequence ((R_EAL f) # x)) . n by MESFUNC8:def_6; hence ((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n by Th1; ::_thesis: verum end; end; theorem :: MESFUN7C:6 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) ) set F = inferior_realsequence f; assume A1: x in dom (f . 0) ; ::_thesis: (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) now__::_thesis:_for_n_being_Element_of_NAT_holds_((inferior_realsequence_f)_#_x)_._n_=_(inferior_realsequence_(R_EAL_(f_#_x)))_._n let n be Element of NAT ; ::_thesis: ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n ( dom ((inferior_realsequence f) . n) = dom (f . 0) & ((inferior_realsequence f) # x) . n = ((inferior_realsequence f) . n) . x ) by Th4, MESFUNC5:def_13; hence ((inferior_realsequence f) # x) . n = (inferior_realsequence (R_EAL (f # x))) . n by A1, Th4; ::_thesis: verum end; hence (inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum end; registration let X be non empty set ; let f be with_the_same_dom Functional_Sequence of X,REAL; cluster R_EAL f -> with_the_same_dom ; coherence R_EAL f is with_the_same_dom proof for n, m being Nat holds dom ((R_EAL f) . n) = dom ((R_EAL f) . m) by MESFUNC8:def_2; hence R_EAL f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum end; end; theorem Th7: :: MESFUN7C:7 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,REAL for S being SigmaField of X for E being Element of S for n being Nat st f . n is_measurable_on E holds (R_EAL f) . n is_measurable_on E proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for S being SigmaField of X for E being Element of S for n being Nat st f . n is_measurable_on E holds (R_EAL f) . n is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for S being SigmaField of X for E being Element of S for n being Nat st f . n is_measurable_on E holds (R_EAL f) . n is_measurable_on E let S be SigmaField of X; ::_thesis: for E being Element of S for n being Nat st f . n is_measurable_on E holds (R_EAL f) . n is_measurable_on E let E be Element of S; ::_thesis: for n being Nat st f . n is_measurable_on E holds (R_EAL f) . n is_measurable_on E let n be Nat; ::_thesis: ( f . n is_measurable_on E implies (R_EAL f) . n is_measurable_on E ) assume f . n is_measurable_on E ; ::_thesis: (R_EAL f) . n is_measurable_on E then R_EAL (f . n) is_measurable_on E by MESFUNC6:def_1; hence (R_EAL f) . n is_measurable_on E ; ::_thesis: verum end; theorem :: MESFUN7C:8 for X being non empty set for f being Functional_Sequence of X,REAL for n being Nat holds (R_EAL f) ^\ n = R_EAL (f ^\ n) ; theorem :: MESFUN7C:9 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,REAL for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n) let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n) let n be Nat; ::_thesis: (inferior_realsequence f) . n = inf (f ^\ n) n in NAT by ORDINAL1:def_12; then (inferior_realsequence (R_EAL f)) . n = inf ((R_EAL f) ^\ n) by MESFUNC8:8; hence (inferior_realsequence f) . n = inf (f ^\ n) ; ::_thesis: verum end; theorem :: MESFUN7C:10 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,REAL for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n) let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n) let n be Nat; ::_thesis: (superior_realsequence f) . n = sup (f ^\ n) n in NAT by ORDINAL1:def_12; then (superior_realsequence (R_EAL f)) . n = sup ((R_EAL f) ^\ n) by MESFUNC8:9; hence (superior_realsequence f) . n = sup (f ^\ n) ; ::_thesis: verum end; theorem Th11: :: MESFUN7C:11 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) holds (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) let x be Element of X; ::_thesis: ( x in dom (f . 0) implies (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) ) set F = superior_realsequence f; assume A1: x in dom (f . 0) ; ::_thesis: (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) now__::_thesis:_for_n_being_Element_of_NAT_holds_((superior_realsequence_f)_#_x)_._n_=_(superior_realsequence_(R_EAL_(f_#_x)))_._n let n be Element of NAT ; ::_thesis: ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n ( dom ((superior_realsequence f) . n) = dom (f . 0) & ((superior_realsequence f) # x) . n = ((superior_realsequence f) . n) . x ) by Th5, MESFUNC5:def_13; hence ((superior_realsequence f) # x) . n = (superior_realsequence (R_EAL (f # x))) . n by A1, Th5; ::_thesis: verum end; hence (superior_realsequence f) # x = superior_realsequence (R_EAL (f # x)) by FUNCT_2:63; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func lim_inf f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 6 lim_inf (R_EAL f); coherence lim_inf (R_EAL f) is PartFunc of X,ExtREAL ; end; :: deftheorem defines lim_inf MESFUN7C:def_6_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf (R_EAL f); theorem Th12: :: MESFUN7C:12 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim_inf f) holds (lim_inf f) . x = lim_inf (R_EAL (f # x)) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim_inf f) holds (lim_inf f) . x = lim_inf (R_EAL (f # x)) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_inf f) holds (lim_inf f) . x = lim_inf (R_EAL (f # x)) let x be Element of X; ::_thesis: ( x in dom (lim_inf f) implies (lim_inf f) . x = lim_inf (R_EAL (f # x)) ) assume x in dom (lim_inf f) ; ::_thesis: (lim_inf f) . x = lim_inf (R_EAL (f # x)) then (lim_inf f) . x = lim_inf ((R_EAL f) # x) by MESFUNC8:def_7; hence (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th1; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func lim_sup f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 7 lim_sup (R_EAL f); coherence lim_sup (R_EAL f) is PartFunc of X,ExtREAL ; end; :: deftheorem defines lim_sup MESFUN7C:def_7_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds lim_sup f = lim_sup (R_EAL f); theorem Th13: :: MESFUN7C:13 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim_sup f) holds (lim_sup f) . x = lim_sup (R_EAL (f # x)) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim_sup f) holds (lim_sup f) . x = lim_sup (R_EAL (f # x)) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim_sup f) holds (lim_sup f) . x = lim_sup (R_EAL (f # x)) let x be Element of X; ::_thesis: ( x in dom (lim_sup f) implies (lim_sup f) . x = lim_sup (R_EAL (f # x)) ) assume x in dom (lim_sup f) ; ::_thesis: (lim_sup f) . x = lim_sup (R_EAL (f # x)) then (lim_sup f) . x = lim_sup ((R_EAL f) # x) by MESFUNC8:def_8; hence (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th1; ::_thesis: verum end; definition let X be non empty set ; let f be Functional_Sequence of X,REAL; func lim f -> PartFunc of X,ExtREAL equals :: MESFUN7C:def 8 lim (R_EAL f); coherence lim (R_EAL f) is PartFunc of X,ExtREAL ; end; :: deftheorem defines lim MESFUN7C:def_8_:_ for X being non empty set for f being Functional_Sequence of X,REAL holds lim f = lim (R_EAL f); theorem Th14: :: MESFUN7C:14 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim f) holds (lim f) . x = lim (R_EAL (f # x)) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim f) holds (lim f) . x = lim (R_EAL (f # x)) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) holds (lim f) . x = lim (R_EAL (f # x)) let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = lim (R_EAL (f # x)) ) assume x in dom (lim f) ; ::_thesis: (lim f) . x = lim (R_EAL (f # x)) then (lim f) . x = lim ((R_EAL f) # x) by MESFUNC8:def_9; hence (lim f) . x = lim (R_EAL (f # x)) by Th1; ::_thesis: verum end; theorem Th15: :: MESFUN7C:15 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (lim f) & f # x is convergent holds ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) let x be Element of X; ::_thesis: ( x in dom (lim f) & f # x is convergent implies ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) ) assume that A1: x in dom (lim f) and A2: f # x is convergent ; ::_thesis: ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) R_EAL (f # x) is convergent by A2, RINFSUP2:14; then A3: ( lim (R_EAL (f # x)) = lim_sup (R_EAL (f # x)) & lim (R_EAL (f # x)) = lim_inf (R_EAL (f # x)) ) by RINFSUP2:41; A4: x in dom (f . 0) by A1, MESFUNC8:def_9; then x in dom (lim_inf f) by MESFUNC8:def_7; then A5: (lim_inf f) . x = lim_inf (R_EAL (f # x)) by Th12; x in dom (lim_sup f) by A4, MESFUNC8:def_8; then (lim_sup f) . x = lim_sup (R_EAL (f # x)) by Th13; hence ( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x ) by A1, A5, A3, Th14; ::_thesis: verum end; theorem :: MESFUN7C:16 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) implies union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ; ::_thesis: union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r))_holds_ x_in_union_(rng_F) let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_dom ((sup f),r)) implies x in union (rng F) ) assume A2: x in (dom (f . 0)) /\ (great_dom ((sup f),r)) ; ::_thesis: x in union (rng F) then reconsider z = x as Element of X ; A3: x in dom (f . 0) by A2, XBOOLE_0:def_4; x in great_dom ((sup f),r) by A2, XBOOLE_0:def_4; then A4: r < (sup f) . z by MESFUNC1:def_13; ex n being Element of NAT st r < (f # z) . n proof assume A5: for n being Element of NAT holds (f # z) . n <= r ; ::_thesis: contradiction for p being ext-real number st p in rng (R_EAL (f # z)) holds p <= r proof let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies p <= r ) assume p in rng (R_EAL (f # z)) ; ::_thesis: p <= r then ex n being set st ( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11; hence p <= r by A5; ::_thesis: verum end; then r is UpperBound of rng (R_EAL (f # z)) by XXREAL_2:def_1; then A6: sup (rng (R_EAL (f # z))) <= r by XXREAL_2:def_3; x in dom (sup f) by A3, MESFUNC8:def_4; hence contradiction by A4, A6, Th3; ::_thesis: verum end; then consider n being Element of NAT such that A7: r < (f # z) . n ; A8: x in dom (f . n) by A3, MESFUNC8:def_2; r < (f . n) . z by A7, SEQFUNC:def_10; then A9: x in great_dom ((f . n),r) by A8, MESFUNC1:def_13; A10: F . n in rng F by FUNCT_2:4; F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1; then x in F . n by A3, A9, XBOOLE_0:def_4; hence x in union (rng F) by A10, TARSKI:def_4; ::_thesis: verum end; then A11: (dom (f . 0)) /\ (great_dom ((sup f),r)) c= union (rng F) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_union_(rng_F)_holds_ x_in_(dom_(f_._0))_/\_(great_dom_((sup_f),r)) let x be set ; ::_thesis: ( x in union (rng F) implies x in (dom (f . 0)) /\ (great_dom ((sup f),r)) ) assume x in union (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_dom ((sup f),r)) then consider y being set such that A12: x in y and A13: y in rng F by TARSKI:def_4; reconsider z = x as Element of X by A12, A13; consider n being set such that A14: n in dom F and A15: y = F . n by A13, FUNCT_1:def_3; reconsider n = n as Element of NAT by A14; A16: F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) by A1; then x in great_dom ((f . n),r) by A12, A15, XBOOLE_0:def_4; then A17: r < (f . n) . z by MESFUNC1:def_13; f # z = (R_EAL f) # z by Th1; then (f . n) . z = ((R_EAL f) # z) . n by SEQFUNC:def_10; then A18: (f . n) . z <= sup (rng ((R_EAL f) # z)) by FUNCT_2:4, XXREAL_2:4; A19: x in dom (f . 0) by A12, A15, A16, XBOOLE_0:def_4; then A20: x in dom (sup f) by MESFUNC8:def_4; then (sup f) . z = sup ((R_EAL f) # z) by MESFUNC8:def_4; then r < (sup f) . z by A17, A18, XXREAL_0:2; then x in great_dom ((sup f),r) by A20, MESFUNC1:def_13; hence x in (dom (f . 0)) /\ (great_dom ((sup f),r)) by A19, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= (dom (f . 0)) /\ (great_dom ((sup f),r)) by TARSKI:def_3; hence union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r)) by A11, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUN7C:17 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for F being SetSequence of S for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) let F be SetSequence of S; ::_thesis: for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) let r be real number ; ::_thesis: ( ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) implies meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ) set E = dom (f . 0); assume A1: for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ; ::_thesis: meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_F)_holds_ x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r)) let x be set ; ::_thesis: ( x in meet (rng F) implies x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ) assume A2: x in meet (rng F) ; ::_thesis: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) then reconsider z = x as Element of X ; A3: F . 0 = (dom (f . 0)) /\ (great_eq_dom ((f . 0),r)) by A1; F . 0 in rng F by FUNCT_2:4; then x in F . 0 by A2, SETFAM_1:def_1; then A4: x in dom (f . 0) by A3, XBOOLE_0:def_4; then A5: x in dom (inf f) by MESFUNC8:def_3; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_(R_EAL_(f_#_z))_._n let n be Element of NAT ; ::_thesis: r <= (R_EAL (f # z)) . n F . n in rng F by FUNCT_2:4; then A7: z in F . n by A2, SETFAM_1:def_1; F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1; then x in great_eq_dom ((f . n),r) by A7, XBOOLE_0:def_4; then r <= (f . n) . z by MESFUNC1:def_14; hence r <= (R_EAL (f # z)) . n by SEQFUNC:def_10; ::_thesis: verum end; for p being ext-real number st p in rng (R_EAL (f # z)) holds r <= p proof let p be ext-real number ; ::_thesis: ( p in rng (R_EAL (f # z)) implies r <= p ) assume p in rng (R_EAL (f # z)) ; ::_thesis: r <= p then ex n being set st ( n in NAT & (R_EAL (f # z)) . n = p ) by FUNCT_2:11; hence r <= p by A6; ::_thesis: verum end; then r is LowerBound of rng (R_EAL (f # z)) by XXREAL_2:def_2; then r <= inf (rng (R_EAL (f # z))) by XXREAL_2:def_4; then r <= (inf f) . x by A5, Th2; then x in great_eq_dom ((inf f),r) by A5, MESFUNC1:def_14; hence x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A4, XBOOLE_0:def_4; ::_thesis: verum end; then A8: meet (rng F) c= (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_(dom_(f_._0))_/\_(great_eq_dom_((inf_f),r))_holds_ x_in_meet_(rng_F) let x be set ; ::_thesis: ( x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) implies x in meet (rng F) ) assume A9: x in (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) ; ::_thesis: x in meet (rng F) then reconsider z = x as Element of X ; A10: x in dom (f . 0) by A9, XBOOLE_0:def_4; x in great_eq_dom ((inf f),r) by A9, XBOOLE_0:def_4; then A11: r <= (inf f) . z by MESFUNC1:def_14; now__::_thesis:_for_y_being_set_st_y_in_rng_F_holds_ x_in_y let y be set ; ::_thesis: ( y in rng F implies x in y ) assume y in rng F ; ::_thesis: x in y then consider n being set such that A12: n in NAT and A13: y = F . n by FUNCT_2:11; reconsider n = n as Element of NAT by A12; A14: x in dom (f . n) by A10, MESFUNC8:def_2; x in dom (inf f) by A10, MESFUNC8:def_3; then A15: (inf f) . z = inf (rng (R_EAL (f # z))) by Th2; (f . n) . z = (R_EAL (f # z)) . n by SEQFUNC:def_10; then (f . n) . z >= inf (rng (R_EAL (f # z))) by FUNCT_2:4, XXREAL_2:3; then r <= (f . n) . z by A11, A15, XXREAL_0:2; then A16: x in great_eq_dom ((f . n),r) by A14, MESFUNC1:def_14; F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) by A1; hence x in y by A10, A13, A16, XBOOLE_0:def_4; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) c= meet (rng F) by TARSKI:def_3; hence meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r)) by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th18: :: MESFUN7C:18 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_sup f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_sup f is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_sup f is_measurable_on E for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7; hence lim_sup f is_measurable_on E by A1, MESFUNC8:23; ::_thesis: verum end; theorem :: MESFUN7C:19 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) holds lim_inf f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) implies lim_inf f is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E ; ::_thesis: lim_inf f is_measurable_on E for n being Nat holds (R_EAL f) . n is_measurable_on E by A2, Th7; hence lim_inf f is_measurable_on E by A1, MESFUNC8:24; ::_thesis: verum end; theorem :: MESFUN7C:20 for X being non empty set for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) & f # x is convergent holds (superior_realsequence f) # x is bounded_below proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,REAL for x being Element of X st x in dom (f . 0) & f # x is convergent holds (superior_realsequence f) # x is bounded_below let f be Functional_Sequence of X,REAL; ::_thesis: for x being Element of X st x in dom (f . 0) & f # x is convergent holds (superior_realsequence f) # x is bounded_below let x be Element of X; ::_thesis: ( x in dom (f . 0) & f # x is convergent implies (superior_realsequence f) # x is bounded_below ) assume A1: x in dom (f . 0) ; ::_thesis: ( not f # x is convergent or (superior_realsequence f) # x is bounded_below ) assume f # x is convergent ; ::_thesis: (superior_realsequence f) # x is bounded_below then A2: f # x is bounded ; then superior_realsequence (R_EAL (f # x)) = superior_realsequence (f # x) by RINFSUP2:9; then A3: (superior_realsequence f) # x = superior_realsequence (f # x) by A1, Th11; superior_realsequence (f # x) is bounded by A2, RINFSUP1:56; hence (superior_realsequence f) # x is bounded_below by A3, RINFSUP2:13; ::_thesis: verum end; theorem Th21: :: MESFUN7C:21 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) implies lim f is_measurable_on E ) assume A1: dom (f . 0) = E ; ::_thesis: ( ex n being Nat st not f . n is_measurable_on E or ex x being Element of X st ( x in E & not f # x is convergent ) or lim f is_measurable_on E ) then A2: dom (lim f) = E by MESFUNC8:def_9; assume for n being Nat holds f . n is_measurable_on E ; ::_thesis: ( ex x being Element of X st ( x in E & not f # x is convergent ) or lim f is_measurable_on E ) then A3: lim_sup f is_measurable_on E by A1, Th18; assume A4: for x being Element of X st x in E holds f # x is convergent ; ::_thesis: lim f is_measurable_on E A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_ (lim_f)_._x_=_(lim_sup_f)_._x let x be Element of X; ::_thesis: ( x in dom (lim f) implies (lim f) . x = (lim_sup f) . x ) assume A6: x in dom (lim f) ; ::_thesis: (lim f) . x = (lim_sup f) . x then f # x is convergent by A2, A4; hence (lim f) . x = (lim_sup f) . x by A6, Th15; ::_thesis: verum end; dom (lim_sup f) = E by A1, MESFUNC8:def_8; hence lim f is_measurable_on E by A2, A3, A5, PARTFUN1:5; ::_thesis: verum end; theorem Th22: :: MESFUN7C:22 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,REAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,REAL for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,REAL; ::_thesis: for g being PartFunc of X,ExtREAL for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let g be PartFunc of X,ExtREAL; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E and A3: dom g = E and A4: for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E A5: dom (lim f) = E by A1, MESFUNC8:def_9; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_f)_holds_ g_._x_=_(lim_f)_._x let x be Element of X; ::_thesis: ( x in dom (lim f) implies g . x = (lim f) . x ) assume A6: x in dom (lim f) ; ::_thesis: g . x = (lim f) . x then x in E by A1, MESFUNC8:def_9; then f # x is convergent by A4; then lim (f # x) = lim (R_EAL (f # x)) by RINFSUP2:14; then g . x = lim (R_EAL (f # x)) by A4, A5, A6; hence g . x = (lim f) . x by A6, Th14; ::_thesis: verum end; then A7: g = lim f by A3, A5, PARTFUN1:5; for x being Element of X st x in E holds f # x is convergent by A4; hence g is_measurable_on E by A1, A2, A7, Th21; ::_thesis: verum end; begin definition let X be non empty set ; let H be Functional_Sequence of X,COMPLEX; let x be Element of X; funcH # x -> Complex_Sequence means :Def9: :: MESFUN7C:def 9 for n being Nat holds it . n = (H . n) . x; existence ex b1 being Complex_Sequence st for n being Nat holds b1 . n = (H . n) . x proof defpred S1[ Element of NAT , set ] means \$2 = (H . \$1) . x; A1: for n being Element of NAT ex y being Element of COMPLEX st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of COMPLEX st S1[n,y] (H . n) . x in COMPLEX by XCMPLX_0:def_2; hence ex y being Element of COMPLEX st S1[n,y] ; ::_thesis: verum end; consider f being Function of NAT,COMPLEX such that A2: for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); take f ; ::_thesis: for n being Nat holds f . n = (H . n) . x let n be Nat; ::_thesis: f . n = (H . n) . x n in NAT by ORDINAL1:def_12; hence f . n = (H . n) . x by A2; ::_thesis: verum end; uniqueness for b1, b2 being Complex_Sequence st ( for n being Nat holds b1 . n = (H . n) . x ) & ( for n being Nat holds b2 . n = (H . n) . x ) holds b1 = b2 proof let S1, S2 be Complex_Sequence; ::_thesis: ( ( for n being Nat holds S1 . n = (H . n) . x ) & ( for n being Nat holds S2 . n = (H . n) . x ) implies S1 = S2 ) assume that A3: for n being Nat holds S1 . n = (H . n) . x and A4: for n being Nat holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2 now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (H . n) . x by A3; hence S1 . n = S2 . n by A4; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines # MESFUN7C:def_9_:_ for X being non empty set for H being Functional_Sequence of X,COMPLEX for x being Element of X for b4 being Complex_Sequence holds ( b4 = H # x iff for n being Nat holds b4 . n = (H . n) . x ); definition let X be non empty set ; let f be Functional_Sequence of X,COMPLEX; func lim f -> PartFunc of X,COMPLEX means :Def10: :: MESFUN7C:def 10 ( dom it = dom (f . 0) & ( for x being Element of X st x in dom it holds it . x = lim (f # x) ) ); existence ex b1 being PartFunc of X,COMPLEX st ( dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim (f # x) ) ) proof defpred S1[ set ] means \$1 in dom (f . 0); deffunc H1( Element of X) -> Element of COMPLEX = lim (f # \$1); consider g being PartFunc of X,COMPLEX such that A1: ( ( for x being Element of X holds ( x in dom g iff S1[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) ) A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_lim_(f_#_x) let x be Element of X; ::_thesis: ( x in dom g implies g . x = lim (f # x) ) assume A3: x in dom g ; ::_thesis: g . x = lim (f # x) then g /. x = lim (f # x) by A1; hence g . x = lim (f # x) by A3, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . 0) ) by A1; hence ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) ) by A2, TARSKI:1; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of X,COMPLEX st dom b1 = dom (f . 0) & ( for x being Element of X st x in dom b1 holds b1 . x = lim (f # x) ) & dom b2 = dom (f . 0) & ( for x being Element of X st x in dom b2 holds b2 . x = lim (f # x) ) holds b1 = b2 proof let g, h be PartFunc of X,COMPLEX; ::_thesis: ( dom g = dom (f . 0) & ( for x being Element of X st x in dom g holds g . x = lim (f # x) ) & dom h = dom (f . 0) & ( for x being Element of X st x in dom h holds h . x = lim (f # x) ) implies g = h ) assume that A4: dom g = dom (f . 0) and A5: for x being Element of X st x in dom g holds g . x = lim (f # x) ; ::_thesis: ( not dom h = dom (f . 0) or ex x being Element of X st ( x in dom h & not h . x = lim (f # x) ) or g = h ) assume that A6: dom h = dom (f . 0) and A7: for x being Element of X st x in dom h holds h . x = lim (f # x) ; ::_thesis: g = h now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_h_._x let x be Element of X; ::_thesis: ( x in dom g implies g . x = h . x ) assume A8: x in dom g ; ::_thesis: g . x = h . x then g . x = lim (f # x) by A5; hence g . x = h . x by A4, A6, A7, A8; ::_thesis: verum end; hence g = h by A4, A6, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def10 defines lim MESFUN7C:def_10_:_ for X being non empty set for f being Functional_Sequence of X,COMPLEX for b3 being PartFunc of X,COMPLEX holds ( b3 = lim f iff ( dom b3 = dom (f . 0) & ( for x being Element of X st x in dom b3 holds b3 . x = lim (f # x) ) ) ); definition let X be non empty set ; let f be Functional_Sequence of X,COMPLEX; func Re f -> Functional_Sequence of X,REAL means :Def11: :: MESFUN7C:def 11 for n being Nat holds ( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds (it . n) . x = (Re (f # x)) . n ) ); existence ex b1 being Functional_Sequence of X,REAL st for n being Nat holds ( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (Re (f # x)) . n ) ) proof defpred S1[ Element of NAT , Function] means ( dom \$2 = dom (f . \$1) & ( for x being Element of X st x in dom \$2 holds \$2 . x = (Re (f # x)) . \$1 ) ); A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y] deffunc H1( Element of X) -> Element of REAL = (Re (f # \$1)) . n; defpred S2[ set ] means \$1 in dom (f . n); consider g being PartFunc of X,REAL such that A2: ( ( for x being Element of X holds ( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] ) A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_(Re_(f_#_x))_._n let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Re (f # x)) . n ) assume A4: x in dom g ; ::_thesis: g . x = (Re (f # x)) . n then g /. x = (Re (f # x)) . n by A2; hence g . x = (Re (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . n) ) by A2; hence ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (X,REAL)) such that A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1); reconsider g = g as Functional_Sequence of X,REAL ; take g ; ::_thesis: for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) thus for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) ::_thesis: verum proof let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) n in NAT by ORDINAL1:def_12; hence ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) by A5; ::_thesis: verum end; end; uniqueness for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds ( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds (b2 . n) . x = (Re (f # x)) . n ) ) ) holds b1 = b2 proof let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (Re (f # x)) . n ) ) ) implies g = h ) assume A6: for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st ( dom (h . n) = dom (f . n) implies ex x being Element of X st ( x in dom (h . n) & not (h . n) . x = (Re (f # x)) . n ) ) or g = h ) assume A7: for n being Nat holds ( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (Re (f # x)) . n ) ) ; ::_thesis: g = h now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n let n be Element of NAT ; ::_thesis: g . n = h . n A8: dom (g . n) = dom (f . n) by A6 .= dom (h . n) by A7 ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_ (g_._n)_._x_=_(h_._n)_._x let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x ) assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x then (g . n) . x = (Re (f # x)) . n by A6; hence (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum end; hence g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum end; hence g = h by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def11 defines Re MESFUN7C:def_11_:_ for X being non empty set for f being Functional_Sequence of X,COMPLEX for b3 being Functional_Sequence of X,REAL holds ( b3 = Re f iff for n being Nat holds ( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds (b3 . n) . x = (Re (f # x)) . n ) ) ); registration let X be non empty set ; let f be with_the_same_dom Functional_Sequence of X,COMPLEX; cluster Re f -> with_the_same_dom ; correctness coherence Re f is with_the_same_dom ; proof now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Re_f)_._k)_=_dom_((Re_f)_._l) let k, l be Nat; ::_thesis: dom ((Re f) . k) = dom ((Re f) . l) dom ((Re f) . k) = dom (f . k) by Def11; then dom ((Re f) . k) = dom (f . l) by MESFUNC8:def_2; hence dom ((Re f) . k) = dom ((Re f) . l) by Def11; ::_thesis: verum end; hence Re f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum end; end; definition let X be non empty set ; let f be Functional_Sequence of X,COMPLEX; func Im f -> Functional_Sequence of X,REAL means :Def12: :: MESFUN7C:def 12 for n being Nat holds ( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds (it . n) . x = (Im (f # x)) . n ) ); existence ex b1 being Functional_Sequence of X,REAL st for n being Nat holds ( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (Im (f # x)) . n ) ) proof defpred S1[ Element of NAT , Function] means ( dom \$2 = dom (f . \$1) & ( for x being Element of X st x in dom \$2 holds \$2 . x = (Im (f # x)) . \$1 ) ); A1: for n being Element of NAT ex y being Element of PFuncs (X,REAL) st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of PFuncs (X,REAL) st S1[n,y] deffunc H1( Element of X) -> Element of REAL = (Im (f # \$1)) . n; defpred S2[ set ] means \$1 in dom (f . n); consider g being PartFunc of X,REAL such that A2: ( ( for x being Element of X holds ( x in dom g iff S2[x] ) ) & ( for x being Element of X st x in dom g holds g /. x = H1(x) ) ) from PARTFUN2:sch_2(); take g ; ::_thesis: ( g is Element of PFuncs (X,REAL) & S1[n,g] ) A3: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_g_holds_ g_._x_=_(Im_(f_#_x))_._n let x be Element of X; ::_thesis: ( x in dom g implies g . x = (Im (f # x)) . n ) assume A4: x in dom g ; ::_thesis: g . x = (Im (f # x)) . n then g /. x = (Im (f # x)) . n by A2; hence g . x = (Im (f # x)) . n by A4, PARTFUN1:def_6; ::_thesis: verum end; for x being set holds ( x in dom g iff x in dom (f . n) ) by A2; hence ( g is Element of PFuncs (X,REAL) & S1[n,g] ) by A3, PARTFUN1:45, TARSKI:1; ::_thesis: verum end; consider g being Function of NAT,(PFuncs (X,REAL)) such that A5: for n being Element of NAT holds S1[n,g . n] from FUNCT_2:sch_3(A1); reconsider g = g as Functional_Sequence of X,REAL ; take g ; ::_thesis: for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) thus for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) ::_thesis: verum proof let n be Nat; ::_thesis: ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) n in NAT by ORDINAL1:def_12; hence ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) by A5; ::_thesis: verum end; end; uniqueness for b1, b2 being Functional_Sequence of X,REAL st ( for n being Nat holds ( dom (b1 . n) = dom (f . n) & ( for x being Element of X st x in dom (b1 . n) holds (b1 . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (b2 . n) = dom (f . n) & ( for x being Element of X st x in dom (b2 . n) holds (b2 . n) . x = (Im (f # x)) . n ) ) ) holds b1 = b2 proof let g, h be Functional_Sequence of X,REAL; ::_thesis: ( ( for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) ) & ( for n being Nat holds ( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (Im (f # x)) . n ) ) ) implies g = h ) assume A6: for n being Nat holds ( dom (g . n) = dom (f . n) & ( for x being Element of X st x in dom (g . n) holds (g . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: ( ex n being Nat st ( dom (h . n) = dom (f . n) implies ex x being Element of X st ( x in dom (h . n) & not (h . n) . x = (Im (f # x)) . n ) ) or g = h ) assume A7: for n being Nat holds ( dom (h . n) = dom (f . n) & ( for x being Element of X st x in dom (h . n) holds (h . n) . x = (Im (f # x)) . n ) ) ; ::_thesis: g = h now__::_thesis:_for_n_being_Element_of_NAT_holds_g_._n_=_h_._n let n be Element of NAT ; ::_thesis: g . n = h . n A8: dom (g . n) = dom (f . n) by A6 .= dom (h . n) by A7 ; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(g_._n)_holds_ (g_._n)_._x_=_(h_._n)_._x let x be Element of X; ::_thesis: ( x in dom (g . n) implies (g . n) . x = (h . n) . x ) assume A9: x in dom (g . n) ; ::_thesis: (g . n) . x = (h . n) . x then (g . n) . x = (Im (f # x)) . n by A6; hence (g . n) . x = (h . n) . x by A7, A8, A9; ::_thesis: verum end; hence g . n = h . n by A8, PARTFUN1:5; ::_thesis: verum end; hence g = h by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def12 defines Im MESFUN7C:def_12_:_ for X being non empty set for f being Functional_Sequence of X,COMPLEX for b3 being Functional_Sequence of X,REAL holds ( b3 = Im f iff for n being Nat holds ( dom (b3 . n) = dom (f . n) & ( for x being Element of X st x in dom (b3 . n) holds (b3 . n) . x = (Im (f # x)) . n ) ) ); registration let X be non empty set ; let f be with_the_same_dom Functional_Sequence of X,COMPLEX; cluster Im f -> with_the_same_dom ; correctness coherence Im f is with_the_same_dom ; proof now__::_thesis:_for_k,_l_being_Nat_holds_dom_((Im_f)_._k)_=_dom_((Im_f)_._l) let k, l be Nat; ::_thesis: dom ((Im f) . k) = dom ((Im f) . l) dom ((Im f) . k) = dom (f . k) by Def12; then dom ((Im f) . k) = dom (f . l) by MESFUNC8:def_2; hence dom ((Im f) . k) = dom ((Im f) . l) by Def12; ::_thesis: verum end; hence Im f is with_the_same_dom by MESFUNC8:def_2; ::_thesis: verum end; end; theorem Th23: :: MESFUN7C:23 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,COMPLEX for x being Element of X st x in dom (f . 0) holds ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX for x being Element of X st x in dom (f . 0) holds ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for x being Element of X st x in dom (f . 0) holds ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) let x be Element of X; ::_thesis: ( x in dom (f . 0) implies ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) ) set F = Re f; set G = Im f; assume A1: x in dom (f . 0) ; ::_thesis: ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_((Re_f)_#_x)_._n_=_(Re_(f_#_x))_._n_&_((Im_f)_#_x)_._n_=_(Im_(f_#_x))_._n_) let n be Element of NAT ; ::_thesis: ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n ) dom ((Re f) . n) = dom (f . n) by Def11; then A2: dom ((Re f) . n) = dom (f . 0) by MESFUNC8:def_2; dom ((Im f) . n) = dom (f . n) by Def12; then A3: dom ((Im f) . n) = dom (f . 0) by MESFUNC8:def_2; ( ((Re f) # x) . n = ((Re f) . n) . x & ((Im f) # x) . n = ((Im f) . n) . x ) by SEQFUNC:def_10; hence ( ((Re f) # x) . n = (Re (f # x)) . n & ((Im f) # x) . n = (Im (f # x)) . n ) by A1, A2, A3, Def11, Def12; ::_thesis: verum end; hence ( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) ) by FUNCT_2:63; ::_thesis: verum end; theorem Th24: :: MESFUN7C:24 for X being non empty set for f being Functional_Sequence of X,COMPLEX for n being Nat holds ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) ) proof let X be non empty set ; ::_thesis: for f being Functional_Sequence of X,COMPLEX for n being Nat holds ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) ) let f be Functional_Sequence of X,COMPLEX; ::_thesis: for n being Nat holds ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) ) let n be Nat; ::_thesis: ( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) ) A1: n in NAT by ORDINAL1:def_12; dom ((Re f) . n) = dom (f . n) by Def11; then A2: dom ((Re f) . n) = dom (Re (f . n)) by COMSEQ_3:def_3; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Re_f)_._n)_holds_ ((Re_f)_._n)_._x_=_(Re_(f_._n))_._x let x be Element of X; ::_thesis: ( x in dom ((Re f) . n) implies ((Re f) . n) . x = (Re (f . n)) . x ) assume A3: x in dom ((Re f) . n) ; ::_thesis: ((Re f) . n) . x = (Re (f . n)) . x then (Re (f . n)) . x = Re ((f . n) . x) by A2, COMSEQ_3:def_3; then A4: (Re (f . n)) . x = Re ((f # x) . n) by Def9; ((Re f) . n) . x = (Re (f # x)) . n by A3, Def11; hence ((Re f) . n) . x = (Re (f . n)) . x by A1, A4, COMSEQ_3:def_5; ::_thesis: verum end; hence (Re f) . n = Re (f . n) by A2, PARTFUN1:5; ::_thesis: (Im f) . n = Im (f . n) dom ((Im f) . n) = dom (f . n) by Def12; then A5: dom ((Im f) . n) = dom (Im (f . n)) by COMSEQ_3:def_4; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((Im_f)_._n)_holds_ ((Im_f)_._n)_._x_=_(Im_(f_._n))_._x let x be Element of X; ::_thesis: ( x in dom ((Im f) . n) implies ((Im f) . n) . x = (Im (f . n)) . x ) assume A6: x in dom ((Im f) . n) ; ::_thesis: ((Im f) . n) . x = (Im (f . n)) . x then (Im (f . n)) . x = Im ((f . n) . x) by A5, COMSEQ_3:def_4; then A7: (Im (f . n)) . x = Im ((f # x) . n) by Def9; ((Im f) . n) . x = (Im (f # x)) . n by A6, Def12; hence ((Im f) . n) . x = (Im (f . n)) . x by A1, A7, COMSEQ_3:def_6; ::_thesis: verum end; hence (Im f) . n = Im (f . n) by A5, PARTFUN1:5; ::_thesis: verum end; theorem Th25: :: MESFUN7C:25 for X being non empty set for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds f # x is convergent ) holds ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) proof let X be non empty set ; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds f # x is convergent ) holds ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: ( ( for x being Element of X st x in dom (f . 0) holds f # x is convergent ) implies ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) ) dom (lim (Re f)) = dom ((Re f) . 0) by MESFUNC8:def_9; then A1: dom (lim (Re f)) = dom (f . 0) by Def11; A2: dom (Re (lim f)) = dom (lim f) by COMSEQ_3:def_3; then A3: dom (lim (Re f)) = dom (Re (lim f)) by A1, Def10; assume A4: for x being Element of X st x in dom (f . 0) holds f # x is convergent ; ::_thesis: ( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) ) A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Re_f))_holds_ (lim_(Re_f))_._x_=_(Re_(lim_f))_._x let x be Element of X; ::_thesis: ( x in dom (lim (Re f)) implies (lim (Re f)) . x = (Re (lim f)) . x ) assume A6: x in dom (lim (Re f)) ; ::_thesis: (lim (Re f)) . x = (Re (lim f)) . x then A7: f # x is convergent by A4, A1; then Re (f # x) is convergent ; then A8: (Re f) # x is convergent by A1, A6, Th23; (lim (Re f)) . x = lim (R_EAL ((Re f) # x)) by A6, Th14 .= lim ((Re f) # x) by A8, RINFSUP2:14 ; then (lim (Re f)) . x = lim (Re (f # x)) by A1, A6, Th23; then A9: (lim (Re f)) . x = Re (lim (f # x)) by A7, COMSEQ_3:41; (Re (lim f)) . x = Re ((lim f) . x) by A3, A6, COMSEQ_3:def_3; hence (lim (Re f)) . x = (Re (lim f)) . x by A2, A3, A6, A9, Def10; ::_thesis: verum end; Re (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7; hence lim (Re f) = Re (lim f) by A3, A5, PARTFUN1:5; ::_thesis: lim (Im f) = Im (lim f) dom (lim (Im f)) = dom ((Im f) . 0) by MESFUNC8:def_9; then A10: dom (lim (Im f)) = dom (f . 0) by Def12; A11: dom (Im (lim f)) = dom (lim f) by COMSEQ_3:def_4; then A12: dom (lim (Im f)) = dom (Im (lim f)) by A10, Def10; A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(Im_f))_holds_ (lim_(Im_f))_._x_=_(Im_(lim_f))_._x let x be Element of X; ::_thesis: ( x in dom (lim (Im f)) implies (lim (Im f)) . x = (Im (lim f)) . x ) assume A14: x in dom (lim (Im f)) ; ::_thesis: (lim (Im f)) . x = (Im (lim f)) . x then A15: f # x is convergent by A4, A10; then Im (f # x) is convergent ; then A16: (Im f) # x is convergent by A10, A14, Th23; (lim (Im f)) . x = lim (R_EAL ((Im f) # x)) by A14, Th14 .= lim ((Im f) # x) by A16, RINFSUP2:14 ; then (lim (Im f)) . x = lim (Im (f # x)) by A10, A14, Th23; then A17: (lim (Im f)) . x = Im (lim (f # x)) by A15, COMSEQ_3:41; (Im (lim f)) . x = Im ((lim f) . x) by A12, A14, COMSEQ_3:def_4; hence (lim (Im f)) . x = (Im (lim f)) . x by A11, A12, A14, A17, Def10; ::_thesis: verum end; Im (lim f) is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7; hence lim (Im f) = Im (lim f) by A12, A13, PARTFUN1:5; ::_thesis: verum end; theorem :: MESFUN7C:26 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) holds lim f is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & ( for x being Element of X st x in E holds f # x is convergent ) implies lim f is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E and A3: for x being Element of X st x in E holds f # x is convergent ; ::_thesis: lim f is_measurable_on E A4: lim (Im f) = R_EAL (Im (lim f)) by A1, A3, Th25; A5: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_ (Im_f)_#_x_is_convergent let x be Element of X; ::_thesis: ( x in E implies (Im f) # x is convergent ) assume A6: x in E ; ::_thesis: (Im f) # x is convergent then f # x is convergent by A3; then Im (f # x) is convergent ; hence (Im f) # x is convergent by A1, A6, Th23; ::_thesis: verum end; A7: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E let n be Nat; ::_thesis: (Im f) . n is_measurable_on E f . n is_measurable_on E by A2; then Im (f . n) is_measurable_on E by MESFUN6C:def_1; hence (Im f) . n is_measurable_on E by Th24; ::_thesis: verum end; dom ((Im f) . 0) = E by A1, Def12; then lim (Im f) is_measurable_on E by A7, A5, Th21; then A8: Im (lim f) is_measurable_on E by A4, MESFUNC6:def_1; A9: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_ (Re_f)_#_x_is_convergent let x be Element of X; ::_thesis: ( x in E implies (Re f) # x is convergent ) assume A10: x in E ; ::_thesis: (Re f) # x is convergent then f # x is convergent by A3; then Re (f # x) is convergent ; hence (Re f) # x is convergent by A1, A10, Th23; ::_thesis: verum end; A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E let n be Nat; ::_thesis: (Re f) . n is_measurable_on E f . n is_measurable_on E by A2; then Re (f . n) is_measurable_on E by MESFUN6C:def_1; hence (Re f) . n is_measurable_on E by Th24; ::_thesis: verum end; A12: lim (Re f) = R_EAL (Re (lim f)) by A1, A3, Th25; dom ((Re f) . 0) = E by A1, Def11; then lim (Re f) is_measurable_on E by A11, A9, Th21; then Re (lim f) is_measurable_on E by A12, MESFUNC6:def_1; hence lim f is_measurable_on E by A8, MESFUN6C:def_1; ::_thesis: verum end; theorem :: MESFUN7C:27 for X being non empty set for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,COMPLEX for g being PartFunc of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being with_the_same_dom Functional_Sequence of X,COMPLEX for g being PartFunc of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let S be SigmaField of X; ::_thesis: for f being with_the_same_dom Functional_Sequence of X,COMPLEX for g being PartFunc of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let f be with_the_same_dom Functional_Sequence of X,COMPLEX; ::_thesis: for g being PartFunc of X,COMPLEX for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) holds g is_measurable_on E let E be Element of S; ::_thesis: ( dom (f . 0) = E & ( for n being Nat holds f . n is_measurable_on E ) & dom g = E & ( for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ) implies g is_measurable_on E ) assume that A1: dom (f . 0) = E and A2: for n being Nat holds f . n is_measurable_on E and A3: dom g = E and A4: for x being Element of X st x in E holds ( f # x is convergent & g . x = lim (f # x) ) ; ::_thesis: g is_measurable_on E A5: now__::_thesis:_for_n_being_Nat_holds_(Im_f)_._n_is_measurable_on_E let n be Nat; ::_thesis: (Im f) . n is_measurable_on E f . n is_measurable_on E by A2; then Im (f . n) is_measurable_on E by MESFUN6C:def_1; hence (Im f) . n is_measurable_on E by Th24; ::_thesis: verum end; A6: dom (Im g) = E by A3, COMSEQ_3:def_4; A7: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_ (_(Im_f)_#_x_is_convergent_&_(Im_g)_._x_=_lim_((Im_f)_#_x)_) let x be Element of X; ::_thesis: ( x in E implies ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) ) assume A8: x in E ; ::_thesis: ( (Im f) # x is convergent & (Im g) . x = lim ((Im f) # x) ) then A9: f # x is convergent by A4; then Im (f # x) is convergent ; hence (Im f) # x is convergent by A1, A8, Th23; ::_thesis: (Im g) . x = lim ((Im f) # x) g . x = lim (f # x) by A4, A8; then Im (g . x) = lim (Im (f # x)) by A9, COMSEQ_3:41; then Im (g . x) = lim ((Im f) # x) by A1, A8, Th23; hence (Im g) . x = lim ((Im f) # x) by A6, A8, COMSEQ_3:def_4; ::_thesis: verum end; dom ((Im f) . 0) = E by A1, Def12; then R_EAL (Im g) is_measurable_on E by A5, A6, A7, Th22; then A10: Im g is_measurable_on E by MESFUNC6:def_1; A11: now__::_thesis:_for_n_being_Nat_holds_(Re_f)_._n_is_measurable_on_E let n be Nat; ::_thesis: (Re f) . n is_measurable_on E f . n is_measurable_on E by A2; then Re (f . n) is_measurable_on E by MESFUN6C:def_1; hence (Re f) . n is_measurable_on E by Th24; ::_thesis: verum end; A12: dom (Re g) = E by A3, COMSEQ_3:def_3; A13: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_ (_(Re_f)_#_x_is_convergent_&_(Re_g)_._x_=_lim_((Re_f)_#_x)_) let x be Element of X; ::_thesis: ( x in E implies ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) ) assume A14: x in E ; ::_thesis: ( (Re f) # x is convergent & (Re g) . x = lim ((Re f) # x) ) then A15: f # x is convergent by A4; then Re (f # x) is convergent ; hence (Re f) # x is convergent by A1, A14, Th23; ::_thesis: (Re g) . x = lim ((Re f) # x) g . x = lim (f # x) by A4, A14; then Re (g . x) = lim (Re (f # x)) by A15, COMSEQ_3:41; then Re (g . x) = lim ((Re f) # x) by A1, A14, Th23; hence (Re g) . x = lim ((Re f) # x) by A12, A14, COMSEQ_3:def_3; ::_thesis: verum end; dom ((Re f) . 0) = E by A1, Def11; then R_EAL (Re g) is_measurable_on E by A11, A12, A13, Th22; then Re g is_measurable_on E by MESFUNC6:def_1; hence g is_measurable_on E by A10, MESFUN6C:def_1; ::_thesis: verum end; begin theorem :: MESFUN7C:28 for X being non empty set for Y being set for f being PartFunc of X,COMPLEX for r being Real holds (r (#) f) | Y = r (#) (f | Y) proof let X be non empty set ; ::_thesis: for Y being set for f being PartFunc of X,COMPLEX for r being Real holds (r (#) f) | Y = r (#) (f | Y) let Y be set ; ::_thesis: for f being PartFunc of X,COMPLEX for r being Real holds (r (#) f) | Y = r (#) (f | Y) let f be PartFunc of X,COMPLEX; ::_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; then dom ((r (#) f) | Y) = (dom f) /\ Y by VALUED_1:def_5; then A2: dom ((r (#) f) | Y) = dom (f | Y) by RELAT_1:61; then A3: dom ((r (#) f) | Y) = dom (r (#) (f | Y)) by VALUED_1:def_5; 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 A5: x in dom (r (#) f) by A1, XBOOLE_0:def_4; thus ((r (#) f) | Y) . x = (r (#) f) . x by A4, FUNCT_1:47 .= r * (f . x) by A5, VALUED_1:def_5 .= r * ((f | Y) . x) by A2, A4, FUNCT_1:47 .= (r (#) (f | Y)) . x by A3, A4, VALUED_1:def_5 ; ::_thesis: verum end; hence (r (#) f) | Y = r (#) (f | Y) by A3, PARTFUN1:5; ::_thesis: verum end; Lm1: for X being non empty set for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative let f be PartFunc of X,COMPLEX; ::_thesis: |.f.| is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_|.f.|_holds_ 0_<=_|.f.|_._x let x be set ; ::_thesis: ( x in dom |.f.| implies 0 <= |.f.| . x ) assume x in dom |.f.| ; ::_thesis: 0 <= |.f.| . x then |.f.| . x = |.(f . x).| by VALUED_1:def_11; hence 0 <= |.f.| . x by COMPLEX1:46; ::_thesis: verum end; hence |.f.| is nonnegative by MESFUNC6:52; ::_thesis: verum end; theorem :: MESFUN7C:29 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for k being real number for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds |.f.| to_power k is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX for k being real number for E being Element of S st 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 f being PartFunc of X,COMPLEX for k being real number for E being Element of S st 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,COMPLEX; ::_thesis: for k being real number for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds |.f.| to_power k is_measurable_on E let k be real number ; ::_thesis: for E being Element of S st 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: ( 0 <= k & E c= dom f & f is_measurable_on E implies |.f.| to_power k is_measurable_on E ) assume that A1: 0 <= k and A2: E c= dom f and A3: f is_measurable_on E ; ::_thesis: |.f.| to_power k is_measurable_on E A4: |.f.| is nonnegative by Lm1; E c= dom |.f.| by A2, VALUED_1:def_11; hence |.f.| to_power k is_measurable_on E by A1, A2, A3, A4, MESFUN6C:29, MESFUN6C:30; ::_thesis: verum end; theorem Th30: :: MESFUN7C:30 for X being non empty set for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) let f, g be PartFunc of X,REAL; ::_thesis: (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) A1: dom ((R_EAL f) (#) (R_EAL g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) by MESFUNC1:def_5; A2: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((R_EAL_f)_(#)_(R_EAL_g))_holds_ ((R_EAL_f)_(#)_(R_EAL_g))_._x_=_(R_EAL_(f_(#)_g))_._x let x be Element of X; ::_thesis: ( x in dom ((R_EAL f) (#) (R_EAL g)) implies ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x ) assume A3: x in dom ((R_EAL f) (#) (R_EAL g)) ; ::_thesis: ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x then x in dom (f (#) g) by A1, VALUED_1:def_4; then A4: (f (#) g) . x = (f . x) * (g . x) by VALUED_1:def_4; ((R_EAL f) (#) (R_EAL g)) . x = ((R_EAL f) . x) * ((R_EAL g) . x) by A3, MESFUNC1:def_5; hence ((R_EAL f) (#) (R_EAL g)) . x = (R_EAL (f (#) g)) . x by A4, EXTREAL1:1; ::_thesis: verum end; dom ((R_EAL f) (#) (R_EAL g)) = dom (R_EAL (f (#) g)) by A1, VALUED_1:def_4; hence (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g) by A2, PARTFUN1:5; ::_thesis: verum end; theorem Th31: :: MESFUN7C:31 for X being non empty set for S being SigmaField of X for E being Element of S for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for E being Element of S for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let S be SigmaField of X; ::_thesis: for E being Element of S for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let E be Element of S; ::_thesis: for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let f, g be PartFunc of X,REAL; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E ) assume that A1: (dom f) /\ (dom g) = E and A2: ( f is_measurable_on E & g is_measurable_on E ) ; ::_thesis: f (#) g is_measurable_on E ( R_EAL f is_measurable_on E & R_EAL g is_measurable_on E ) by A2, MESFUNC6:def_1; then (R_EAL f) (#) (R_EAL g) is_measurable_on E by A1, MESFUNC7:15; then R_EAL (f (#) g) is_measurable_on E by Th30; hence f (#) g is_measurable_on E by MESFUNC6:def_1; ::_thesis: verum end; theorem Th32: :: MESFUN7C:32 for X being non empty set for f, g being PartFunc of X,COMPLEX holds ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re 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) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) ) A1: dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def_4; A2: dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def_4; A3: dom (Re f) = dom f by COMSEQ_3:def_3; A4: dom (Im g) = dom g by COMSEQ_3:def_4; A5: dom (Re g) = dom g by COMSEQ_3:def_3; A6: dom (Re (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_3; then A7: dom (Re (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4; A8: dom (Im f) = dom f by COMSEQ_3:def_4; A9: dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g))) by VALUED_1:12; now__::_thesis:_for_x_being_set_st_x_in_dom_(Re_(f_(#)_g))_holds_ (Re_(f_(#)_g))_._x_=_(((Re_f)_(#)_(Re_g))_-_((Im_f)_(#)_(Im_g)))_._x let x be set ; ::_thesis: ( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x ) assume A10: x in dom (Re (f (#) g)) ; ::_thesis: (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im 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 A6, A10, VALUED_1:def_4; then A11: (Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x))) by COMPLEX1:9; x in dom g by A7, A10, XBOOLE_0:def_4; then A12: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4; x in dom f by A7, A10, XBOOLE_0:def_4; then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4; then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x)) by A7, A1, A3, A5, A10, A11, A12, VALUED_1:def_4; then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x) by A7, A2, A8, A4, A10, VALUED_1:def_4; hence (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x by A7, A9, A1, A2, A3, A8, A5, A4, A10, VALUED_1:13; ::_thesis: verum end; hence Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) by A7, A9, A1, A2, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) A13: dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g)) by VALUED_1:def_4; A14: dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g)) by VALUED_1:def_4; A15: dom (Im (f (#) g)) = dom (f (#) g) by COMSEQ_3:def_4; then A16: dom (Im (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def_4; A17: dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g))) by VALUED_1:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_(Im_(f_(#)_g))_holds_ (Im_(f_(#)_g))_._x_=_(((Im_f)_(#)_(Re_g))_+_((Re_f)_(#)_(Im_g)))_._x let x be set ; ::_thesis: ( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x ) assume A18: x in dom (Im (f (#) g)) ; ::_thesis: (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re 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 A15, A18, VALUED_1:def_4; then A19: (Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x))) by COMPLEX1:9; x in dom g by A16, A18, XBOOLE_0:def_4; then A20: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def_3, COMSEQ_3:def_4; x in dom f by A16, A18, XBOOLE_0:def_4; then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def_3, COMSEQ_3:def_4; then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x)) by A16, A13, A8, A5, A18, A19, A20, VALUED_1:def_4; then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x) by A16, A14, A3, A4, A18, VALUED_1:def_4; hence (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x by A16, A17, A13, A14, A3, A8, A5, A4, A18, VALUED_1:def_1; ::_thesis: verum end; hence Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1:2; ::_thesis: verum end; theorem :: MESFUN7C:33 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,COMPLEX for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,COMPLEX for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,COMPLEX for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let f, g be PartFunc of X,COMPLEX; ::_thesis: for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds f (#) g is_measurable_on E let E be Element of S; ::_thesis: ( (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E implies f (#) g is_measurable_on E ) assume that A1: (dom f) /\ (dom g) = E and A2: f is_measurable_on E and A3: g is_measurable_on E ; ::_thesis: f (#) g is_measurable_on E A4: dom (Im g) = dom g by COMSEQ_3:def_4; A5: Im f is_measurable_on E by A2, MESFUN6C:def_1; A6: dom (Im f) = dom f by COMSEQ_3:def_4; then A7: dom ((Im f) (#) (Im g)) = E by A1, A4, VALUED_1:def_4; A8: Im g is_measurable_on E by A3, MESFUN6C:def_1; then A9: (Im f) (#) (Im g) is_measurable_on E by A1, A5, A6, A4, Th31; A10: dom (Re f) = dom f by COMSEQ_3:def_3; A11: dom (Re g) = dom g by COMSEQ_3:def_3; A12: Re g is_measurable_on E by A3, MESFUN6C:def_1; then A13: (Im f) (#) (Re g) is_measurable_on E by A1, A5, A6, A11, Th31; A14: Re f is_measurable_on E by A2, MESFUN6C:def_1; then (Re f) (#) (Im g) is_measurable_on E by A1, A8, A10, A4, Th31; then ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) is_measurable_on E by A13, MESFUNC6:26; then A15: Im (f (#) g) is_measurable_on E by Th32; (Re f) (#) (Re g) is_measurable_on E by A1, A14, A12, A10, A11, Th31; then ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) is_measurable_on E by A9, A7, MESFUNC6:29; then Re (f (#) g) is_measurable_on E by Th32; hence f (#) g is_measurable_on E by A15, MESFUN6C:def_1; ::_thesis: verum end; theorem Th34: :: MESFUN7C: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 ex E being Element of S st ( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds g . x <= f . x ) holds Integral (M,g) <= 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, g being PartFunc of X,REAL st ex E being Element of S st ( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds g . x <= f . x ) holds Integral (M,g) <= Integral (M,f) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,REAL st ex E being Element of S st ( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds g . x <= f . x ) holds Integral (M,g) <= Integral (M,f) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,REAL st ex E being Element of S st ( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds g . x <= f . x ) holds Integral (M,g) <= Integral (M,f) let f, g be PartFunc of X,REAL; ::_thesis: ( ex E being Element of S st ( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds g . x <= f . x ) implies Integral (M,g) <= Integral (M,f) ) assume that A1: ex A being Element of S st ( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) and A2: ( f is nonnegative & g is nonnegative ) and A3: for x being Element of X st x in dom g holds g . x <= f . x ; ::_thesis: Integral (M,g) <= Integral (M,f) A4: ( Integral (M,g) = integral+ (M,(R_EAL g)) & Integral (M,f) = integral+ (M,(R_EAL f)) ) by A1, A2, MESFUNC6:82; consider A being Element of S such that A5: ( A = dom f & A = dom g ) and A6: ( f is_measurable_on A & g is_measurable_on A ) by A1; ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by A6, MESFUNC6:def_1; hence Integral (M,g) <= Integral (M,f) by A2, A3, A5, A4, MESFUNC5:85; ::_thesis: verum end; theorem Th35: :: MESFUN7C:35 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 ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.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 f is_integrable_on M holds ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.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 f is_integrable_on M holds ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) ) assume A1: f is_integrable_on M ; ::_thesis: ( ex A being Element of S st ( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M ) then Re f is_integrable_on M by MESFUN6C:def_2; then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4; then consider A1 being Element of S such that A2: A1 = dom (R_EAL (Re f)) and A3: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17; A4: Re f is_measurable_on A1 by A3, MESFUNC6:def_1; Im f is_integrable_on M by A1, MESFUN6C:def_2; then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4; then consider A2 being Element of S such that A5: A2 = dom (R_EAL (Im f)) and A6: R_EAL (Im f) is_measurable_on A2 by MESFUNC5:def_17; A7: A1 = dom f by A2, COMSEQ_3:def_3; A2 = dom f by A5, COMSEQ_3:def_4; then Im f is_measurable_on A1 by A6, A7, MESFUNC6:def_1; then A8: f is_measurable_on A1 by A4, MESFUN6C:def_1; hence ex A being Element of S st ( A = dom f & f is_measurable_on A ) by A7; ::_thesis: |.f.| is_integrable_on M thus |.f.| is_integrable_on M by A1, A7, A8, MESFUN6C:31; ::_thesis: verum end; theorem :: MESFUN7C:36 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 ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) let M be sigma_Measure of S; ::_thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M implies ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) ) assume A1: f is_integrable_on M ; ::_thesis: ex F being Function of NAT,S st ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) then consider E being Element of S such that A2: E = dom f and A3: f is_measurable_on E by Th35; defpred S1[ Element of NAT , set ] means \$2 = E /\ (great_eq_dom (|.f.|,(1 / (\$1 + 1)))); A4: dom |.f.| = E by A2, VALUED_1:def_11; now__::_thesis:_for_x_being_set_st_x_in_E_\_(eq_dom_(|.f.|,0))_holds_ x_in_E_/\_(great_dom_(|.f.|,0)) let x be set ; ::_thesis: ( x in E \ (eq_dom (|.f.|,0)) implies x in E /\ (great_dom (|.f.|,0)) ) reconsider y = |.f.| . x as Real ; assume A5: x in E \ (eq_dom (|.f.|,0)) ; ::_thesis: x in E /\ (great_dom (|.f.|,0)) then A6: x in E by XBOOLE_0:def_5; then A7: x in dom |.f.| by A2, VALUED_1:def_11; not x in eq_dom (|.f.|,0) by A5, XBOOLE_0:def_5; then not y = 0 by A7, MESFUNC6:7; then not |.(f . x).| = 0 by A7, VALUED_1:def_11; then f . x <> 0 by COMPLEX1:5, SQUARE_1:17; then 0 < |.(f . x).| by COMPLEX1:47; then 0 < |.f.| . x by A7, VALUED_1:def_11; then x in great_dom (|.f.|,0) by A7, MESFUNC1:def_13; hence x in E /\ (great_dom (|.f.|,0)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A8: E \ (eq_dom (|.f.|,0)) c= E /\ (great_dom (|.f.|,0)) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_E_/\_(great_dom_(|.f.|,0))_holds_ x_in_E_\_(eq_dom_(|.f.|,0)) let x be set ; ::_thesis: ( x in E /\ (great_dom (|.f.|,0)) implies x in E \ (eq_dom (|.f.|,0)) ) assume A9: x in E /\ (great_dom (|.f.|,0)) ; ::_thesis: x in E \ (eq_dom (|.f.|,0)) then x in great_dom (|.f.|,0) by XBOOLE_0:def_4; then 0 < |.f.| . x by MESFUNC1:def_13; then A10: not x in eq_dom (|.f.|,0) by MESFUNC1:def_15; x in E by A9, XBOOLE_0:def_4; hence x in E \ (eq_dom (|.f.|,0)) by A10, XBOOLE_0:def_5; ::_thesis: verum end; then A11: E /\ (great_dom (|.f.|,0)) c= E \ (eq_dom (|.f.|,0)) by TARSKI:def_3; A12: |.f.| is_measurable_on E by A2, A3, MESFUN6C:30; A13: for n being Element of NAT ex Z being Element of S st S1[n,Z] proof let n be Element of NAT ; ::_thesis: ex Z being Element of S st S1[n,Z] take E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) ; ::_thesis: ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) thus ( E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) is Element of S & S1[n,E /\ (great_eq_dom (|.f.|,(1 / (n + 1))))] ) by A12, A4, MESFUNC6:13; ::_thesis: verum end; consider F being Function of NAT,S such that A14: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A13); A15: for n being Nat holds ( F . n in S & M . (F . n) < +infty ) proof |.f.| is_integrable_on M by A1, Th35; then A16: Integral (M,|.f.|) < +infty by MESFUNC6:90; let n be Nat; ::_thesis: ( F . n in S & M . (F . n) < +infty ) reconsider n1 = n as Element of NAT by ORDINAL1:def_12; set z = R_EAL (1 / (n + 1)); A17: F . n1 = E /\ (great_eq_dom (|.f.|,(1 / (n1 + 1)))) by A14; then reconsider En = F . n as Element of S ; set h = |.f.| | En; consider nf being PartFunc of X,REAL such that A18: nf is_simple_func_in S and A19: dom nf = En and A20: for x being set st x in En holds nf . x = 1 / (n + 1) by MESFUNC6:75; A21: dom (|.f.| | En) = En by A4, A17, RELAT_1:62, XBOOLE_1:17; A22: F . n c= great_eq_dom (|.f.|,(1 / (n + 1))) by A17, XBOOLE_1:17; A23: for x being Element of X st x in dom nf holds nf . x <= (|.f.| | En) . x proof let x be Element of X; ::_thesis: ( x in dom nf implies nf . x <= (|.f.| | En) . x ) assume A24: x in dom nf ; ::_thesis: nf . x <= (|.f.| | En) . x then (|.f.| | En) . x = |.f.| . x by A19, FUNCT_1:49; then 1 / (n + 1) <= (|.f.| | En) . x by A22, A19, A24, MESFUNC1:def_14; hence nf . x <= (|.f.| | En) . x by A19, A20, A24; ::_thesis: verum end; (dom |.f.|) /\ En = E /\ En by A2, VALUED_1:def_11; then A25: (dom |.f.|) /\ En = En by A17, XBOOLE_1:17, XBOOLE_1:28; |.f.| is_measurable_on En by A12, A17, MESFUNC6:16, XBOOLE_1:17; then A26: |.f.| | En is_measurable_on En by A25, MESFUNC6:76; A27: |.f.| | En is nonnegative by Lm1, MESFUNC6:55; for x being set st x in dom nf holds nf . x >= 0 by A19, A20; then A28: nf is nonnegative by MESFUNC6:52; ( |.f.| is nonnegative & |.f.| | E = |.f.| ) by A4, Lm1, RELAT_1:69; then A29: Integral (M,(|.f.| | En)) <= Integral (M,|.f.|) by A12, A4, A17, MESFUNC6:87, XBOOLE_1:17; nf is_measurable_on En by A18, MESFUNC6:50; then Integral (M,nf) <= Integral (M,(|.f.| | En)) by A21, A26, A27, A19, A28, A23, Th34; then A30: Integral (M,nf) <= Integral (M,|.f.|) by A29, XXREAL_0:2; A31: ( ((R_EAL (1 / (n + 1))) * (M . En)) / (R_EAL (1 / (n + 1))) = M . En & +infty / (R_EAL (1 / (n + 1))) = +infty ) by XXREAL_3:83, XXREAL_3:88; Integral (M,nf) = (R_EAL (1 / (n + 1))) * (M . En) by A19, A20, MESFUNC6:97; then (R_EAL (1 / (n + 1))) * (M . En) < +infty by A16, A30, XXREAL_0:2; hence ( F . n in S & M . (F . n) < +infty ) by A31, XXREAL_3:80; ::_thesis: verum end; take F ; ::_thesis: ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) A32: for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) proof let n be Nat; ::_thesis: F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) n in NAT by ORDINAL1:def_12; hence F . n = E /\ (great_eq_dom (|.f.|,(1 / (n + 1)))) by A14; ::_thesis: verum end; then for n being Nat holds F . n = E /\ (great_eq_dom (|.f.|,(0 + (1 / (n + 1))))) ; then E /\ (great_dom (|.f.|,0)) = union (rng F) by MESFUNC6:11; hence ( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds ( F . n in S & M . (F . n) < +infty ) ) ) by A2, A32, A11, A8, A15, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th37: :: MESFUN7C:37 for X being non empty set for f being PartFunc of X,COMPLEX for A being set holds |.f.| | A = |.(f | A).| proof let X be non empty set ; ::_thesis: for f being PartFunc of X,COMPLEX for A being set holds |.f.| | A = |.(f | A).| let f be PartFunc of X,COMPLEX; ::_thesis: for A being set holds |.f.| | A = |.(f | A).| let A be set ; ::_thesis: |.f.| | A = |.(f | A).| dom (|.f.| | A) = (dom |.f.|) /\ A by RELAT_1:61; then A1: dom (|.f.| | A) = (dom f) /\ A by VALUED_1:def_11; A2: dom (f | A) = (dom f) /\ A by RELAT_1:61; then A3: dom |.(f | A).| = (dom f) /\ A by VALUED_1:def_11; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(|.f.|_|_A)_holds_ (|.f.|_|_A)_._x_=_|.(f_|_A).|_._x let x be Element of X; ::_thesis: ( x in dom (|.f.| | A) implies (|.f.| | A) . x = |.(f | A).| . x ) assume A4: x in dom (|.f.| | A) ; ::_thesis: (|.f.| | A) . x = |.(f | A).| . x then |.(f | A).| . x = |.((f | A) . x).| by A1, A3, VALUED_1:def_11; then A5: |.(f | A).| . x = |.(f . x).| by A2, A1, A4, FUNCT_1:47; x in dom f by A1, A4, XBOOLE_0:def_4; then A6: x in dom |.f.| by VALUED_1:def_11; (|.f.| | A) . x = |.f.| . x by A4, FUNCT_1:47; hence (|.f.| | A) . x = |.(f | A).| . x by A6, A5, VALUED_1:def_11; ::_thesis: verum end; hence |.f.| | A = |.(f | A).| by A1, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th38: :: MESFUN7C:38 for X being non empty set for f, g being PartFunc of X,COMPLEX holds ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| ) dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1; then dom (|.f.| + |.g.|) = (dom f) /\ (dom |.g.|) by VALUED_1:def_11; hence dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by VALUED_1:def_11; ::_thesis: dom |.(f + g).| c= dom |.f.| dom |.(f + g).| = dom (f + g) by VALUED_1:def_11 .= (dom f) /\ (dom g) by VALUED_1:def_1 ; then dom |.(f + g).| c= dom f by XBOOLE_1:17; hence dom |.(f + g).| c= dom |.f.| by VALUED_1:def_11; ::_thesis: verum end; theorem Th39: :: MESFUN7C:39 for X being non empty set for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) let f, g be PartFunc of X,COMPLEX; ::_thesis: (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) A1: dom |.(f + g).| c= dom |.g.| by Th38; then A2: dom |.(f + g).| c= dom g by VALUED_1:def_11; dom (g | (dom |.(f + g).|)) = (dom g) /\ (dom |.(f + g).|) by RELAT_1:61; then A3: dom (g | (dom |.(f + g).|)) = dom |.(f + g).| by A2, XBOOLE_1:28; then A4: dom |.(g | (dom |.(f + g).|)).| = dom |.(f + g).| by VALUED_1:def_11; A5: dom |.(f + g).| c= dom |.f.| by Th38; then A6: dom |.(f + g).| c= dom f by VALUED_1:def_11; then (dom |.(f + g).|) /\ (dom |.(f + g).|) c= (dom f) /\ (dom g) by A2, XBOOLE_1:27; then A7: dom |.(f + g).| c= dom (|.f.| + |.g.|) by Th38; then A8: dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) = dom |.(f + g).| by RELAT_1:62; dom (f | (dom |.(f + g).|)) = (dom f) /\ (dom |.(f + g).|) by RELAT_1:61; then A9: dom (f | (dom |.(f + g).|)) = dom |.(f + g).| by A6, XBOOLE_1:28; A10: ( |.f.| | (dom |.(f + g).|) = |.(f | (dom |.(f + g).|)).| & |.g.| | (dom |.(f + g).|) = |.(g | (dom |.(f + g).|)).| ) by Th37; then A11: dom ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) = (dom (f | (dom |.(f + g).|))) /\ (dom (g | (dom |.(f + g).|))) by Th38 .= dom |.(f + g).| by A9, A3 ; A12: dom |.(f | (dom |.(f + g).|)).| = dom |.(f + g).| by A9, VALUED_1:def_11; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_holds_ ((|.f.|_+_|.g.|)_|_(dom_|.(f_+_g).|))_._x_=_((|.f.|_|_(dom_|.(f_+_g).|))_+_(|.g.|_|_(dom_|.(f_+_g).|)))_._x let x be Element of X; ::_thesis: ( x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) implies ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x ) assume A13: x in dom ((|.f.| + |.g.|) | (dom |.(f + g).|)) ; ::_thesis: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x then A14: ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = (|.f.| + |.g.|) . x by FUNCT_1:47 .= (|.f.| . x) + (|.g.| . x) by A7, A8, A13, VALUED_1:def_1 .= |.(f . x).| + (|.g.| . x) by A5, A8, A13, VALUED_1:def_11 ; A15: x in dom |.(f + g).| by A7, A13, RELAT_1:62; then ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x = ((|.f.| | (dom |.(f + g).|)) . x) + ((|.g.| | (dom |.(f + g).|)) . x) by A11, VALUED_1:def_1 .= |.((f | (dom |.(f + g).|)) . x).| + (|.(g | (dom |.(f + g).|)).| . x) by A12, A10, A15, VALUED_1:def_11 .= |.((f | (dom |.(f + g).|)) . x).| + |.((g | (dom |.(f + g).|)) . x).| by A4, A15, VALUED_1:def_11 .= |.(f . x).| + |.((g | (dom |.(f + g).|)) . x).| by A15, FUNCT_1:49 .= |.(f . x).| + |.(g . x).| by A15, FUNCT_1:49 ; hence ((|.f.| + |.g.|) | (dom |.(f + g).|)) . x = ((|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|))) . x by A1, A8, A13, A14, VALUED_1:def_11; ::_thesis: verum end; hence (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|) by A11, A7, PARTFUN1:5, RELAT_1:62; ::_thesis: verum end; theorem Th40: :: MESFUN7C:40 for X being non empty set for f, g being PartFunc of X,COMPLEX for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,COMPLEX for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x let f, g be PartFunc of X,COMPLEX; ::_thesis: for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x let x be set ; ::_thesis: ( x in dom |.(f + g).| implies |.(f + g).| . x <= (|.f.| + |.g.|) . x ) A1: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by COMPLEX1:56; assume A2: x in dom |.(f + g).| ; ::_thesis: |.(f + g).| . x <= (|.f.| + |.g.|) . x then x in dom (f + g) by VALUED_1:def_11; then A3: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by A1, VALUED_1:def_1; A4: dom |.(f + g).| c= dom |.g.| by Th38; then A5: |.(g . x).| = |.g.| . x by A2, VALUED_1:def_11; x in dom |.g.| by A2, A4; then A6: x in dom g by VALUED_1:def_11; A7: dom |.(f + g).| c= dom |.f.| by Th38; then x in dom |.f.| by A2; then x in dom f by VALUED_1:def_11; then x in (dom f) /\ (dom g) by A6, XBOOLE_0:def_4; then A8: x in dom (|.f.| + |.g.|) by Th38; |.(f . x).| = |.f.| . x by A2, A7, VALUED_1:def_11; then |.(f . x).| + |.(g . x).| = (|.f.| + |.g.|) . x by A5, A8, VALUED_1:def_1; hence |.(f + g).| . x <= (|.f.| + |.g.|) . x by A2, A3, VALUED_1:def_11; ::_thesis: verum end; theorem Th41: :: MESFUN7C:41 for X being non empty set for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds f . x <= g . x ) holds g - f is nonnegative proof let X be non empty set ; ::_thesis: for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds f . x <= g . x ) holds g - f is nonnegative let f, g be PartFunc of X,REAL; ::_thesis: ( ( for x being set st x in dom f holds f . x <= g . x ) implies g - f is nonnegative ) assume A1: for x being set st x in dom f holds f . x <= g . x ; ::_thesis: g - f is nonnegative now__::_thesis:_for_x_being_set_st_x_in_dom_(g_-_f)_holds_ 0_<=_(g_-_f)_._x let x be set ; ::_thesis: ( x in dom (g - f) implies 0 <= (g - f) . x ) assume A2: x in dom (g - f) ; ::_thesis: 0 <= (g - f) . x then x in (dom g) /\ (dom f) by VALUED_1:12; then x in dom f by XBOOLE_0:def_4; then 0 <= (g . x) - (f . x) by A1, XREAL_1:48; hence 0 <= (g - f) . x by A2, VALUED_1:13; ::_thesis: verum end; hence g - f is nonnegative by MESFUNC6:52; ::_thesis: verum end; theorem :: MESFUN7C: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,COMPLEX st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) let f, g be PartFunc of X,COMPLEX; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) ( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, A2, Th35; then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC6:100; Im g is_integrable_on M by A2, MESFUN6C:def_2; then R_EAL (Im g) is_integrable_on M by MESFUNC6:def_4; then consider B2 being Element of S such that A4: ( B2 = dom (R_EAL (Im g)) & R_EAL (Im g) is_measurable_on B2 ) by MESFUNC5:def_17; Im f is_integrable_on M by A1, MESFUN6C:def_2; then R_EAL (Im f) is_integrable_on M by MESFUNC6:def_4; then consider A2 being Element of S such that A5: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is_measurable_on A2 ) by MESFUNC5:def_17; Re g is_integrable_on M by A2, MESFUN6C:def_2; then R_EAL (Re g) is_integrable_on M by MESFUNC6:def_4; then consider B1 being Element of S such that A6: B1 = dom (R_EAL (Re g)) and A7: R_EAL (Re g) is_measurable_on B1 by MESFUNC5:def_17; A8: B1 = dom g by A6, COMSEQ_3:def_3; f + g is_integrable_on M by A1, A2, MESFUN6C:33; then A9: |.(f + g).| is_integrable_on M by Th35; set G = |.g.|; set F = |.f.|; for x being set st x in dom |.(f + g).| holds |.(f + g).| . x <= (|.f.| + |.g.|) . x by Th40; then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41; Re f is_integrable_on M by A1, MESFUN6C:def_2; then R_EAL (Re f) is_integrable_on M by MESFUNC6:def_4; then consider A1 being Element of S such that A11: A1 = dom (R_EAL (Re f)) and A12: R_EAL (Re f) is_measurable_on A1 by MESFUNC5:def_17; A13: A1 = dom f by A11, COMSEQ_3:def_3; reconsider A = A1 /\ B1 as Element of S ; Re f is_measurable_on A1 by A12, MESFUNC6:def_1; then A14: Re f is_measurable_on A by MESFUNC6:16, XBOOLE_1:17; A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; then A16: dom |.(f + g).| = A by A13, A8, VALUED_1:def_11; Re g is_measurable_on B1 by A7, MESFUNC6:def_1; then A17: Re g is_measurable_on A by MESFUNC6:16, XBOOLE_1:17; ( B2 = dom g & Im g is_measurable_on B2 ) by A4, COMSEQ_3:def_4, MESFUNC6:def_1; then Im g is_measurable_on A by A8, MESFUNC6:16, XBOOLE_1:17; then A18: g is_measurable_on A by A17, MESFUN6C:def_1; then A19: |.g.| is_measurable_on A by A8, MESFUN6C:30, XBOOLE_1:17; ( A2 = dom f & Im f is_measurable_on A2 ) by A5, COMSEQ_3:def_4, MESFUNC6:def_1; then Im f is_measurable_on A by A13, MESFUNC6:16, XBOOLE_1:17; then A20: f is_measurable_on A by A14, MESFUN6C:def_1; then |.f.| is_measurable_on A by A13, MESFUN6C:30, XBOOLE_1:17; then A21: |.f.| + |.g.| is_measurable_on A by A19, MESFUNC6:26; A c= A1 by XBOOLE_1:17; then A22: A c= dom |.f.| by A13, VALUED_1:def_11; A c= B1 by XBOOLE_1:17; then A23: A c= dom |.g.| by A8, VALUED_1:def_11; A24: dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def_1; then A25: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by A22, A23, A16, XBOOLE_1:19, XBOOLE_1:28; |.(f + g).| is_measurable_on A by A13, A8, A20, A18, A15, MESFUN6C:11, MESFUN6C:30; then consider E being Element of S such that A26: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A21, A3, A25, A9, A10, MESFUN6C:42; A28: dom (|.g.| | E) = E by A23, A25, A26, RELAT_1:62; take E ; ::_thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) thus E = dom (f + g) by A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; ::_thesis: Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by A1, A2, Th35, MESFUNC6:91; then consider E1 being Element of S such that A29: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and A30: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by MESFUNC6:101; dom (|.f.| | E) = E by A22, A25, A26, RELAT_1:62; then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A29, A28, FUNCT_1:51; hence Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; ::_thesis: verum end; begin definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,COMPLEX; predf is_simple_func_in S means :Def13: :: MESFUN7C:def 13 ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ); end; :: deftheorem Def13 defines is_simple_func_in MESFUN7C:def_13_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st ( dom f = union (rng F) & ( for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y ) ) ); definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,REAL; let F be Finite_Sep_Sequence of S; let a be FinSequence of REAL ; predF,a are_Re-presentation_of f means :Def14: :: MESFUN7C:def 14 ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ); end; :: deftheorem Def14 defines are_Re-presentation_of MESFUN7C:def_14_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,REAL for F being Finite_Sep_Sequence of S for a being FinSequence of REAL holds ( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) ); definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,COMPLEX; let F be Finite_Sep_Sequence of S; let a be FinSequence of COMPLEX ; predF,a are_Re-presentation_of f means :Def15: :: MESFUN7C:def 15 ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ); end; :: deftheorem Def15 defines are_Re-presentation_of MESFUN7C:def_15_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for F being Finite_Sep_Sequence of S for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) ); theorem :: MESFUN7C:43 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) ) hereby ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S implies f is_simple_func_in S ) assume f is_simple_func_in S ; ::_thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S ) then consider F being Finite_Sep_Sequence of S such that A1: dom f = union (rng F) and A2: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y by Def13; A3: dom (Im f) = union (rng F) by A1, COMSEQ_3:def_4; A4: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (Im f) . x = (Im f) . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (Im f) . x = (Im f) . y let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Im f) . x = (Im f) . y ) assume that A5: n in dom F and A6: ( x in F . n & y in F . n ) ; ::_thesis: (Im f) . x = (Im f) . y F . n c= union (rng F) by A5, MESFUNC3:7; then ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A3, A6, COMSEQ_3:def_4; hence (Im f) . x = (Im f) . y by A2, A5, A6; ::_thesis: verum end; A7: dom (Re f) = union (rng F) by A1, COMSEQ_3:def_3; for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (Re f) . x = (Re f) . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (Re f) . x = (Re f) . y let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies (Re f) . x = (Re f) . y ) assume that A8: n in dom F and A9: ( x in F . n & y in F . n ) ; ::_thesis: (Re f) . x = (Re f) . y F . n c= union (rng F) by A8, MESFUNC3:7; then ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A7, A9, COMSEQ_3:def_3; hence (Re f) . x = (Re f) . y by A2, A8, A9; ::_thesis: verum end; hence ( Re f is_simple_func_in S & Im f is_simple_func_in S ) by A7, A3, A4, MESFUNC6:def_2; ::_thesis: verum end; assume that A10: Re f is_simple_func_in S and A11: Im f is_simple_func_in S ; ::_thesis: f is_simple_func_in S consider F being Finite_Sep_Sequence of S such that A12: dom (Re f) = union (rng F) and A13: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds (Re f) . x = (Re f) . y by A10, MESFUNC6:def_2; set la = len F; A14: dom f = union (rng F) by A12, COMSEQ_3:def_3; consider G being Finite_Sep_Sequence of S such that A15: dom (Im f) = union (rng G) and A16: for n being Nat for x, y being Element of X st n in dom G & x in G . n & y in G . n holds (Im f) . x = (Im f) . y by A11, MESFUNC6:def_2; set lb = len G; deffunc H1( Nat) -> set = (F . (((\$1 -' 1) div (len G)) + 1)) /\ (G . (((\$1 -' 1) mod (len G)) + 1)); consider FG being FinSequence such that A17: len FG = (len F) * (len G) and A18: for k being Nat st k in dom FG holds FG . k = H1(k) from FINSEQ_1:sch_2(); A19: dom FG = Seg ((len F) * (len G)) by A17, FINSEQ_1:def_3; now__::_thesis:_for_k_being_Nat_st_k_in_dom_FG_holds_ FG_._k_in_S let k be Nat; ::_thesis: ( k in dom FG implies FG . k in S ) A20: len G divides (len F) * (len G) by NAT_D:def_3; set j = ((k -' 1) mod (len G)) + 1; set i = ((k -' 1) div (len G)) + 1; assume A21: k in dom FG ; ::_thesis: FG . k in S then A22: 1 <= k by FINSEQ_3:25; then A23: len G > 0 by A17, A21, FINSEQ_3:25; A24: k <= (len F) * (len G) by A17, A21, FINSEQ_3:25; then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; then A25: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24; A26: 1 <= (len F) * (len G) by A22, A24, XXREAL_0:2; 1 <= len G by A23, NAT_1:14; then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A26, A20, NAT_2:15; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A25, XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A23, NAT_1:14, NAT_D:18; then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25; then A27: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:3; (k -' 1) mod (len G) < len G by A23, NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14; then ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25; then G . (((k -' 1) mod (len G)) + 1) in rng G by FUNCT_1:3; then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A27, MEASURE1:34; hence FG . k in S by A18, A21; ::_thesis: verum end; then reconsider FG = FG as FinSequence of S by FINSEQ_2:12; for k, l being Nat st k in dom FG & l in dom FG & k <> l holds FG . k misses FG . l proof let k, l be Nat; ::_thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l ) assume that A28: k in dom FG and A29: l in dom FG and A30: k <> l ; ::_thesis: FG . k misses FG . l set m = ((l -' 1) mod (len G)) + 1; set n = ((l -' 1) div (len G)) + 1; A31: 1 <= k by A28, FINSEQ_3:25; then A32: len G > 0 by A17, A28, FINSEQ_3:25; then A33: (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by NAT_D:2; A34: k <= (len F) * (len G) by A17, A28, FINSEQ_3:25; then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A31, NAT_1:14, NAT_D:def_3; 1 <= len G by A32, NAT_1:14; then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A35, NAT_2:15; set j = ((k -' 1) mod (len G)) + 1; set i = ((k -' 1) div (len G)) + 1; FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A28; then A37: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A18, A29 .= (F . (((k -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16 .= (F . (((k -' 1) div (len G)) + 1)) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1)))) by XBOOLE_1:16 .= ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by XBOOLE_1:16 ; l <= (len F) * (len G) by A17, A29, FINSEQ_3:25; then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24; then ((l -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((l -' 1) div (len G)) + 1 >= 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:14, NAT_D:18; then ((l -' 1) div (len G)) + 1 in Seg (len F) ; then A38: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; 1 <= l by A29, FINSEQ_3:25; then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A33, XREAL_1:233; (l -' 1) mod (len G) < len G by A32, NAT_D:1; then ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14; then ((l -' 1) mod (len G)) + 1 in Seg (len G) ; then A40: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3; k -' 1 <= ((len F) * (len G)) -' 1 by A34, NAT_D:42; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:11, NAT_D:18; then ((k -' 1) div (len G)) + 1 in Seg (len F) ; then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def_3; (k -' 1) + 1 = ((((((k -' 1) div (len G)) + 1) - 1) * (len G)) + ((((k -' 1) mod (len G)) + 1) - 1)) + 1 by A32, NAT_D:2; then A42: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by A31, XREAL_1:233; (k -' 1) mod (len G) < len G by A32, NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:11, NAT_1:13; then ((k -' 1) mod (len G)) + 1 in Seg (len G) ; then A43: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def_3; percases ( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by A30, A42, A39; suppose ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 ; ::_thesis: FG . k misses FG . l then F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1) by A41, A38, MESFUNC3:4; then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A37, XBOOLE_0:def_7; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; suppose ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ; ::_thesis: FG . k misses FG . l then G . (((k -' 1) mod (len G)) + 1) misses G . (((l -' 1) mod (len G)) + 1) by A43, A40, MESFUNC3:4; then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A37, XBOOLE_0:def_7; hence FG . k misses FG . l by XBOOLE_0:def_7; ::_thesis: verum end; end; end; then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4; A44: dom f = union (rng G) by A15, COMSEQ_3:def_4; A45: dom f = union (rng FG) proof thus dom f c= union (rng FG) :: according to XBOOLE_0:def_10 ::_thesis: union (rng FG) c= dom f proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in dom f or z in union (rng FG) ) assume A46: z in dom f ; ::_thesis: z in union (rng FG) then consider Y being set such that A47: z in Y and A48: Y in rng F by A14, TARSKI:def_4; consider Z being set such that A49: z in Z and A50: Z in rng G by A44, A46, TARSKI:def_4; consider j being Nat such that A51: j in dom G and A52: Z = G . j by A50, FINSEQ_2:10; consider i being Nat such that A53: i in dom F and A54: F . i = Y by A48, FINSEQ_2:10; 1 <= i by A53, FINSEQ_3:25; then consider i9 being Nat such that A55: i = 1 + i9 by NAT_1:10; set k = ((i - 1) * (len G)) + j; reconsider k = ((i - 1) * (len G)) + j as Nat by A55; i <= len F by A53, FINSEQ_3:25; then i - 1 <= (len F) - 1 by XREAL_1:9; then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64; then A56: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6; A57: j <= len G by A51, FINSEQ_3:25; then (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by XREAL_1:6; then A58: k <= (len F) * (len G) by A56, XXREAL_0:2; A59: 1 <= j by A51, FINSEQ_3:25; then consider j9 being Nat such that A60: j = 1 + j9 by NAT_1:10; A61: j9 < len G by A57, A60, NAT_1:13; A62: k >= j by A55, NAT_1:11; then A63: k -' 1 = k - 1 by A59, XREAL_1:233, XXREAL_0:2 .= (i9 * (len G)) + j9 by A55, A60 ; then A64: i = ((k -' 1) div (len G)) + 1 by A55, A61, NAT_D:def_1; A65: k >= 1 by A59, A62, XXREAL_0:2; then A66: k in Seg ((len F) * (len G)) by A58, FINSEQ_1:1; A67: j = ((k -' 1) mod (len G)) + 1 by A60, A63, A61, NAT_D:def_2; k in dom FG by A17, A65, A58, FINSEQ_3:25; then A68: FG . k in rng FG by FUNCT_1:def_3; z in (F . i) /\ (G . j) by A47, A54, A49, A52, XBOOLE_0:def_4; then z in FG . k by A18, A19, A64, A67, A66; hence z in union (rng FG) by A68, TARSKI:def_4; ::_thesis: verum end; let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union (rng FG) or z in dom f ) assume z in union (rng FG) ; ::_thesis: z in dom f then consider Y being set such that A69: z in Y and A70: Y in rng FG by TARSKI:def_4; consider k being Nat such that A71: k in dom FG and A72: FG . k = Y by A70, FINSEQ_2:10; A73: 1 <= k by A71, FINSEQ_3:25; then A74: len G > 0 by A17, A71, FINSEQ_3:25; then A75: 1 <= len G by NAT_1:14; A76: k <= (len F) * (len G) by A17, A71, FINSEQ_3:25; then ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A73, NAT_1:14, NAT_D:def_3; then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A75, NAT_2:15; set j = ((k -' 1) mod (len G)) + 1; set i = ((k -' 1) div (len G)) + 1; k -' 1 <= ((len F) * (len G)) -' 1 by A76, NAT_D:42; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A77, NAT_2:24; then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by NAT_1:14, XREAL_1:19; ((len F) * (len G)) div (len G) = len F by A74, NAT_D:18; then ((k -' 1) div (len G)) + 1 in dom F by A78, FINSEQ_3:25; then A79: F . (((k -' 1) div (len G)) + 1) in rng F by FUNCT_1:def_3; FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A71; then z in F . (((k -' 1) div (len G)) + 1) by A69, A72, XBOOLE_0:def_4; hence z in dom f by A14, A79, TARSKI:def_4; ::_thesis: verum end; for k being Nat for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds f . x = f . y proof let k be Nat; ::_thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds f . x = f . y let x, y be Element of X; ::_thesis: ( k in dom FG & x in FG . k & y in FG . k implies f . x = f . y ) set i = ((k -' 1) div (len G)) + 1; set j = ((k -' 1) mod (len G)) + 1; assume that A80: k in dom FG and A81: ( x in FG . k & y in FG . k ) ; ::_thesis: f . x = f . y A82: FG . k c= union (rng FG) by A80, MESFUNC3:7; then FG . k c= dom (Im f) by A45, COMSEQ_3:def_4; then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A81, COMSEQ_3:def_4; A84: 1 <= k by A80, FINSEQ_3:25; then A85: len G > 0 by A17, A80, FINSEQ_3:25; then (k -' 1) mod (len G) < len G by NAT_D:1; then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14; then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25; FG . k c= dom (Re f) by A45, A82, COMSEQ_3:def_3; then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A81, COMSEQ_3:def_3; A88: k <= (len F) * (len G) by A17, A80, FINSEQ_3:25; then A89: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42; A90: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A80; then ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by A81, XBOOLE_0:def_4; then A91: Im (f . x) = Im (f . y) by A16, A86, A83; A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A84, A88, NAT_1:14, NAT_D:def_3; 1 <= len G by A85, NAT_1:14; then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A92, NAT_2:15; then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A89, NAT_2:24; then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by XREAL_1:19; then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_1:14, NAT_D:18; then A93: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25; ( x in F . (((k -' 1) div (len G)) + 1) & y in F . (((k -' 1) div (len G)) + 1) ) by A81, A90, XBOOLE_0:def_4; then Re (f . x) = Re (f . y) by A13, A93, A87; hence f . x = f . y by A91, COMPLEX1:def_3; ::_thesis: verum end; hence f is_simple_func_in S by A45, Def13; ::_thesis: verum end; theorem Th44: :: MESFUN7C:44 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) then consider F being Finite_Sep_Sequence of S such that A1: dom f = union (rng F) and A2: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y by Def13; defpred S1[ set , set ] means for x being set st x in F . \$1 holds \$2 = f . x; A3: for k being Nat st k in Seg (len F) holds ex y being Element of COMPLEX st S1[k,y] proof let k be Nat; ::_thesis: ( k in Seg (len F) implies ex y being Element of COMPLEX st S1[k,y] ) assume k in Seg (len F) ; ::_thesis: ex y being Element of COMPLEX st S1[k,y] then A4: k in dom F by FINSEQ_1:def_3; then A5: F . k in rng F by FUNCT_1:3; percases ( F . k = {} or F . k <> {} ) ; supposeA6: F . k = {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y] reconsider y = 0 as Element of COMPLEX by NUMBERS:11, TARSKI:def_3; take y ; ::_thesis: S1[k,y] thus S1[k,y] by A6; ::_thesis: verum end; suppose F . k <> {} ; ::_thesis: ex y being Element of COMPLEX st S1[k,y] then consider x1 being set such that A7: x1 in F . k by XBOOLE_0:def_1; x1 in dom f by A1, A5, A7, TARSKI:def_4; then f . x1 in rng f by FUNCT_1:3; then reconsider y = f . x1 as Element of COMPLEX ; take y ; ::_thesis: S1[k,y] hereby ::_thesis: verum let x be set ; ::_thesis: ( x in F . k implies y = f . x ) A8: rng F c= bool X by XBOOLE_1:1; assume x in F . k ; ::_thesis: y = f . x hence y = f . x by A2, A4, A5, A7, A8; ::_thesis: verum end; end; end; end; consider a being FinSequence of COMPLEX such that A9: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds S1[k,a . k] ) ) from FINSEQ_1:sch_5(A3); take F ; ::_thesis: ex a being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) take a ; ::_thesis: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) now__::_thesis:_for_n_being_Nat_st_n_in_dom_F_holds_ for_x_being_set_st_x_in_F_._n_holds_ a_._n_=_f_._x let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds a . n = f . x ) assume n in dom F ; ::_thesis: for x being set st x in F . n holds a . n = f . x then n in Seg (len F) by FINSEQ_1:def_3; hence for x being set st x in F . n holds a . n = f . x by A9; ::_thesis: verum end; hence ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) by A1, A9, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th45: :: MESFUN7C:45 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f ) hereby ::_thesis: ( ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f implies f is_simple_func_in S ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f then consider F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A1: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n ) ) by Th44; take F = F; ::_thesis: ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f take a = a; ::_thesis: F,a are_Re-presentation_of f thus F,a are_Re-presentation_of f by A1, Def15; ::_thesis: verum end; given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A2: F,a are_Re-presentation_of f ; ::_thesis: f is_simple_func_in S A3: for n being Nat for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y proof let n be Nat; ::_thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds f . x = f . y let x, y be Element of X; ::_thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y ) assume that A4: n in dom F and A5: x in F . n and A6: y in F . n ; ::_thesis: f . x = f . y f . x = a . n by A2, A4, A5, Def15; hence f . x = f . y by A2, A4, A6, Def15; ::_thesis: verum end; dom f = union (rng F) by A2, Def15; hence f is_simple_func_in S by A3, Def13; ::_thesis: verum end; theorem Th46: :: MESFUN7C:46 for c being FinSequence of COMPLEX for n being Nat st n in dom (Re c) holds (Re c) . n = Re (c . n) proof let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Re c) holds (Re c) . n = Re (c . n) let n be Nat; ::_thesis: ( n in dom (Re c) implies (Re c) . n = Re (c . n) ) A1: ((1 / 2) * (c *')) . n = (1 / 2) * ((c *') . n) by COMPLSP2:16; ( len ((1 / 2) * c) = len c & len ((1 / 2) * (c *')) = len (c *') ) by COMPLSP2:3; then A2: len ((1 / 2) * c) = len ((1 / 2) * (c *')) by COMPLSP2:def_1; len (c *') = len c by COMPLSP2:def_1; then ( n in NAT & (1 / 2) * (c + (c *')) = ((1 / 2) * c) + ((1 / 2) * (c *')) ) by COMPLSP2:30, ORDINAL1:def_12; then A3: (Re c) . n = (((1 / 2) * c) . n) + (((1 / 2) * (c *')) . n) by A2, COMPLSP2:26; assume A4: n in dom (Re c) ; ::_thesis: (Re c) . n = Re (c . n) then n <= len (Re c) by FINSEQ_3:25; then A5: n <= len c by COMPLSP2:48; 1 <= n by A4, FINSEQ_3:25; then ((1 / 2) * (c *')) . n = (1 / 2) * ((c . n) *') by A5, A1, COMPLSP2:def_1; then A6: (Re c) . n = ((1 / 2) * (c . n)) + ((1 / 2) * ((c . n) *')) by A3, COMPLSP2:16; c . n = (Re (c . n)) + ((Im (c . n)) * ) by COMPLEX1:13; hence (Re c) . n = Re (c . n) by A6; ::_thesis: verum end; theorem Th47: :: MESFUN7C:47 for c being FinSequence of COMPLEX for n being Nat st n in dom (Im c) holds (Im c) . n = Im (c . n) proof let c be FinSequence of COMPLEX ; ::_thesis: for n being Nat st n in dom (Im c) holds (Im c) . n = Im (c . n) let n be Nat; ::_thesis: ( n in dom (Im c) implies (Im c) . n = Im (c . n) ) assume A1: n in dom (Im c) ; ::_thesis: (Im c) . n = Im (c . n) then A2: 1 <= n by FINSEQ_3:25; n <= len (Im c) by A1, FINSEQ_3:25; then A3: n <= len c by COMPLSP2:48; A4: ((- ((1 / 2) * )) * (c *')) . n = (- ((1 / 2) * )) * ((c *') . n) by COMPLSP2:16 .= (- ((1 / 2) * )) * ((c . n) *') by A2, A3, COMPLSP2:def_1 ; ( len ((- ((1 / 2) * )) * c) = len c & len ((- ((1 / 2) * )) * (c *')) = len (c *') ) by COMPLSP2:3; then A5: len ((- ((1 / 2) * )) * c) = len ((- ((1 / 2) * )) * (c *')) by COMPLSP2:def_1; len (c *') = len c by COMPLSP2:def_1; then ( n in NAT & (- ((1 / 2) * )) * (c - (c *')) = ((- ((1 / 2) * )) * c) - ((- ((1 / 2) * )) * (c *')) ) by COMPLSP2:43, ORDINAL1:def_12; then (Im c) . n = (((- ((1 / 2) * )) * c) . n) - (((- ((1 / 2) * )) * (c *')) . n) by A5, COMPLSP2:25; then A6: (Im c) . n = ((- ((1 / 2) * )) * (c . n)) - ((- ((1 / 2) * )) * ((c . n) *')) by A4, COMPLSP2:16; (c . n) - ((c . n) *') = ((Re (c . n)) + ((Im (c . n)) * )) - ((Re (c . n)) - ((Im (c . n)) * )) by COMPLEX1:13; hence (Im c) . n = Im (c . n) by A6; ::_thesis: verum end; theorem Th48: :: MESFUN7C:48 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX for F being Finite_Sep_Sequence of S for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX for F being Finite_Sep_Sequence of S for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX for F being Finite_Sep_Sequence of S for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) let f be PartFunc of X,COMPLEX; ::_thesis: for F being Finite_Sep_Sequence of S for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) let F be Finite_Sep_Sequence of S; ::_thesis: for a being FinSequence of COMPLEX holds ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) let a be FinSequence of COMPLEX ; ::_thesis: ( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) ) hereby ::_thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f implies F,a are_Re-presentation_of f ) assume A1: F,a are_Re-presentation_of f ; ::_thesis: ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) len (Im a) = len a by COMPLSP2:48; then dom (Im a) = Seg (len a) by FINSEQ_1:def_3; then dom (Im a) = dom a by FINSEQ_1:def_3; then A2: dom F = dom (Im a) by A1, Def15; dom (Im f) = dom f by COMSEQ_3:def_4; then A3: dom (Im f) = union (rng F) by A1, Def15; A4: for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im a) . n proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds (Im f) . x = (Im a) . n ) assume A5: n in dom F ; ::_thesis: for x being set st x in F . n holds (Im f) . x = (Im a) . n let x be set ; ::_thesis: ( x in F . n implies (Im f) . x = (Im a) . n ) assume A6: x in F . n ; ::_thesis: (Im f) . x = (Im a) . n F . n c= union (rng F) by A5, MESFUNC3:7; then x in dom (Im f) by A3, A6; then A7: (Im f) . x = Im (f . x) by COMSEQ_3:def_4; Im (f . x) = Im (a . n) by A1, A5, A6, Def15; hence (Im f) . x = (Im a) . n by A2, A5, A7, Th47; ::_thesis: verum end; len (Re a) = len a by COMPLSP2:48; then dom (Re a) = Seg (len a) by FINSEQ_1:def_3; then dom (Re a) = dom a by FINSEQ_1:def_3; then A8: dom F = dom (Re a) by A1, Def15; dom (Re f) = dom f by COMSEQ_3:def_3; then A9: dom (Re f) = union (rng F) by A1, Def15; for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re a) . n proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds (Re f) . x = (Re a) . n ) assume A10: n in dom F ; ::_thesis: for x being set st x in F . n holds (Re f) . x = (Re a) . n let x be set ; ::_thesis: ( x in F . n implies (Re f) . x = (Re a) . n ) assume A11: x in F . n ; ::_thesis: (Re f) . x = (Re a) . n F . n c= union (rng F) by A10, MESFUNC3:7; then x in dom (Re f) by A9, A11; then A12: (Re f) . x = Re (f . x) by COMSEQ_3:def_3; Re (f . x) = Re (a . n) by A1, A10, A11, Def15; hence (Re f) . x = (Re a) . n by A8, A10, A12, Th46; ::_thesis: verum end; hence ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) by A9, A3, A8, A2, A4, Def14; ::_thesis: verum end; assume that A13: F, Re a are_Re-presentation_of Re f and A14: F, Im a are_Re-presentation_of Im f ; ::_thesis: F,a are_Re-presentation_of f A15: dom F = dom (Re a) by A13, Def14; A16: dom (Re f) = union (rng F) by A13, Def14; then A17: dom f = union (rng F) by COMSEQ_3:def_3; A18: dom F = dom (Im a) by A14, Def14; A19: dom (Im f) = union (rng F) by A14, Def14; A20: for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = a . n proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds f . x = a . n ) assume A21: n in dom F ; ::_thesis: for x being set st x in F . n holds f . x = a . n let x be set ; ::_thesis: ( x in F . n implies f . x = a . n ) assume A22: x in F . n ; ::_thesis: f . x = a . n A23: F . n c= union (rng F) by A21, MESFUNC3:7; then x in dom (Im f) by A19, A22; then A24: (Im f) . x = Im (f . x) by COMSEQ_3:def_4; x in dom (Re f) by A16, A22, A23; then A25: (Re f) . x = Re (f . x) by COMSEQ_3:def_3; (Im f) . x = (Im a) . n by A14, A21, A22, Def14; then A26: Im (f . x) = Im (a . n) by A18, A21, A24, Th47; (Re f) . x = (Re a) . n by A13, A21, A22, Def14; then Re (f . x) = Re (a . n) by A15, A21, A25, Th46; hence f . x = a . n by A26, COMPLEX1:def_3; ::_thesis: verum end; len (Re a) = len a by COMPLSP2:48; then dom (Re a) = Seg (len a) by FINSEQ_1:def_3; then dom F = dom a by A15, FINSEQ_1:def_3; hence F,a are_Re-presentation_of f by A17, A20, Def15; ::_thesis: verum end; theorem :: MESFUN7C:49 for X being non empty set for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,COMPLEX holds ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) ) let f be PartFunc of X,COMPLEX; ::_thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) ) hereby ::_thesis: ( ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) implies f is_simple_func_in S ) assume f is_simple_func_in S ; ::_thesis: ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) then consider F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A1: F,c are_Re-presentation_of f by Th45; F, Im c are_Re-presentation_of Im f by A1, Th48; then A2: for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n by Def14; F, Re c are_Re-presentation_of Re f by A1, Th48; then A3: for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n by Def14; ( dom f = union (rng F) & dom F = dom c ) by A1, Def15; hence ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st ( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ) ) by A3, A2; ::_thesis: verum end; given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A4: dom f = union (rng F) and A5: dom F = dom c and A6: for n being Nat st n in dom F holds for x being set st x in F . n holds (Re f) . x = (Re c) . n and A7: for n being Nat st n in dom F holds for x being set st x in F . n holds (Im f) . x = (Im c) . n ; ::_thesis: f is_simple_func_in S A8: dom (Im f) = union (rng F) by A4, COMSEQ_3:def_4; len (Im c) = len c by COMPLSP2:48; then dom (Im c) = Seg (len c) by FINSEQ_1:def_3; then A9: dom F = dom (Im c) by A5, FINSEQ_1:def_3; len (Re c) = len c by COMPLSP2:48; then dom (Re c) = Seg (len c) by FINSEQ_1:def_3; then A10: dom F = dom (Re c) by A5, FINSEQ_1:def_3; A11: dom (Re f) = union (rng F) by A4, COMSEQ_3:def_3; for n being Nat st n in dom F holds for x being set st x in F . n holds f . x = c . n proof let n be Nat; ::_thesis: ( n in dom F implies for x being set st x in F . n holds f . x = c . n ) assume A12: n in dom F ; ::_thesis: for x being set st x in F . n holds f . x = c . n let x be set ; ::_thesis: ( x in F . n implies f . x = c . n ) assume A13: x in F . n ; ::_thesis: f . x = c . n A14: F . n c= union (rng F) by A12, MESFUNC3:7; then x in dom (Im f) by A8, A13; then A15: (Im f) . x = Im (f . x) by COMSEQ_3:def_4; x in dom (Re f) by A11, A13, A14; then A16: (Re f) . x = Re (f . x) by COMSEQ_3:def_3; (Im f) . x = (Im c) . n by A7, A12, A13; then A17: Im (f . x) = Im (c . n) by A9, A12, A15, Th47; (Re f) . x = (Re c) . n by A6, A12, A13; then Re (f . x) = Re (c . n) by A10, A12, A16, Th46; hence f . x = c . n by A17, COMPLEX1:def_3; ::_thesis: verum end; then F,c are_Re-presentation_of f by A4, A5, Def15; hence f is_simple_func_in S by Th45; ::_thesis: verum end;