:: MESFUN10 semantic presentation begin theorem Th1: :: MESFUN10:1 for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds inf (rng seq1) <= inf (rng seq2) proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies inf (rng seq1) <= inf (rng seq2) ) assume A1: for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: inf (rng seq1) <= inf (rng seq2) now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq2_holds_ inf_(rng_seq1)_<=_x let x be ext-real number ; ::_thesis: ( x in rng seq2 implies inf (rng seq1) <= x ) A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_inf_(rng_seq1)_<=_seq2_._n let n be Element of NAT ; ::_thesis: inf (rng seq1) <= seq2 . n dom seq1 = NAT by FUNCT_2:def_1; then A3: seq1 . n in rng seq1 by FUNCT_1:def_3; A4: seq1 . n <= seq2 . n by A1; inf (rng seq1) is LowerBound of rng seq1 by XXREAL_2:def_4; then inf (rng seq1) <= seq1 . n by A3, XXREAL_2:def_2; hence inf (rng seq1) <= seq2 . n by A4, XXREAL_0:2; ::_thesis: verum end; assume x in rng seq2 ; ::_thesis: inf (rng seq1) <= x then ex z being set st ( z in dom seq2 & x = seq2 . z ) by FUNCT_1:def_3; hence inf (rng seq1) <= x by A2; ::_thesis: verum end; then inf (rng seq1) is LowerBound of rng seq2 by XXREAL_2:def_2; hence inf (rng seq1) <= inf (rng seq2) by XXREAL_2:def_4; ::_thesis: verum end; theorem Th2: :: MESFUN10:2 for seq1, seq2 being ExtREAL_sequence for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: for k being Nat st ( for n being Nat holds seq1 . n <= seq2 . n ) holds ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) let k be Nat; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) ) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; assume A1: for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) A2: now__::_thesis:_for_n_being_Nat_holds_(seq1_^\_k1)_._n_<=_(seq2_^\_k1)_._n let n be Nat; ::_thesis: (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n A3: (seq2 ^\ k1) . n = seq2 . (n + k) by NAT_1:def_3; (seq1 ^\ k1) . n = seq1 . (n + k) by NAT_1:def_3; hence (seq1 ^\ k1) . n <= (seq2 ^\ k1) . n by A1, A3; ::_thesis: verum end; then sup (seq1 ^\ k1) <= sup (seq2 ^\ k1) by MESFUNC5:55; then A4: (superior_realsequence seq1) . k <= sup (seq2 ^\ k1) by RINFSUP2:27; inf (seq1 ^\ k1) <= inf (seq2 ^\ k1) by A2, Th1; then (inferior_realsequence seq1) . k <= inf (seq2 ^\ k1) by RINFSUP2:27; hence ( (inferior_realsequence seq1) . k <= (inferior_realsequence seq2) . k & (superior_realsequence seq1) . k <= (superior_realsequence seq2) . k ) by A4, RINFSUP2:27; ::_thesis: verum end; theorem Th3: :: MESFUN10:3 for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n <= seq2 . n ) holds ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n <= seq2 . n ) implies ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) ) assume for n being Nat holds seq1 . n <= seq2 . n ; ::_thesis: ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) then for n being Nat holds ( (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n & (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) by Th2; hence ( lim_inf seq1 <= lim_inf seq2 & lim_sup seq1 <= lim_sup seq2 ) by Th1, MESFUNC5:55; ::_thesis: verum end; theorem Th4: :: MESFUN10:4 for seq being ExtREAL_sequence for a being R_eal st ( for n being Nat holds seq . n >= a ) holds inf seq >= a proof let seq be ExtREAL_sequence; ::_thesis: for a being R_eal st ( for n being Nat holds seq . n >= a ) holds inf seq >= a let a be R_eal; ::_thesis: ( ( for n being Nat holds seq . n >= a ) implies inf seq >= a ) assume A1: for n being Nat holds seq . n >= a ; ::_thesis: inf seq >= a now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq_holds_ x_>=_a let x be ext-real number ; ::_thesis: ( x in rng seq implies x >= a ) assume x in rng seq ; ::_thesis: x >= a then ex z being set st ( z in dom seq & x = seq . z ) by FUNCT_1:def_3; hence x >= a by A1; ::_thesis: verum end; then a is LowerBound of rng seq by XXREAL_2:def_2; hence inf seq >= a by XXREAL_2:def_4; ::_thesis: verum end; theorem Th5: :: MESFUN10:5 for seq being ExtREAL_sequence for a being R_eal st ( for n being Nat holds seq . n <= a ) holds sup seq <= a proof let seq be ExtREAL_sequence; ::_thesis: for a being R_eal st ( for n being Nat holds seq . n <= a ) holds sup seq <= a let a be R_eal; ::_thesis: ( ( for n being Nat holds seq . n <= a ) implies sup seq <= a ) assume A1: for n being Nat holds seq . n <= a ; ::_thesis: sup seq <= a now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_seq_holds_ x_<=_a let x be ext-real number ; ::_thesis: ( x in rng seq implies x <= a ) assume x in rng seq ; ::_thesis: x <= a then ex z being set st ( z in dom seq & x = seq . z ) by FUNCT_1:def_3; hence x <= a by A1; ::_thesis: verum end; then a is UpperBound of rng seq by XXREAL_2:def_1; hence sup seq <= a by XXREAL_2:def_3; ::_thesis: verum end; theorem Th6: :: MESFUN10:6 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for x being Element of X for n being Element of NAT st x in dom (inf (F ^\ n)) holds (inf (F ^\ n)) . x = inf ((F # x) ^\ n) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for x being Element of X for n being Element of NAT st x in dom (inf (F ^\ n)) holds (inf (F ^\ n)) . x = inf ((F # x) ^\ n) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for x being Element of X for n being Element of NAT st x in dom (inf (F ^\ n)) holds (inf (F ^\ n)) . x = inf ((F # x) ^\ n) let x be Element of X; ::_thesis: for n being Element of NAT st x in dom (inf (F ^\ n)) holds (inf (F ^\ n)) . x = inf ((F # x) ^\ n) let n be Element of NAT ; ::_thesis: ( x in dom (inf (F ^\ n)) implies (inf (F ^\ n)) . x = inf ((F # x) ^\ n) ) now__::_thesis:_for_k_being_Element_of_NAT_holds_((F_^\_n)_#_x)_._k_=_((F_#_x)_^\_n)_._k reconsider g = F as Function of NAT,(PFuncs (X,ExtREAL)) ; let k be Element of NAT ; ::_thesis: ((F ^\ n) # x) . k = ((F # x) ^\ n) . k ((F ^\ n) # x) . k = ((F ^\ n) . k) . x by MESFUNC5:def_13; then ((F ^\ n) # x) . k = (g . (n + k)) . x by NAT_1:def_3; then ((F ^\ n) # x) . k = (F # x) . (n + k) by MESFUNC5:def_13; hence ((F ^\ n) # x) . k = ((F # x) ^\ n) . k by NAT_1:def_3; ::_thesis: verum end; then A1: (F ^\ n) # x = (F # x) ^\ n by FUNCT_2:63; assume x in dom (inf (F ^\ n)) ; ::_thesis: (inf (F ^\ n)) . x = inf ((F # x) ^\ n) hence (inf (F ^\ n)) . x = inf ((F # x) ^\ n) by A1, MESFUNC8:def_3; ::_thesis: verum end; theorem Th7: :: MESFUN10:7 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) let M be sigma_Measure of S; ::_thesis: for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) let E be Element of S; ::_thesis: ( E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) implies ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) ) assume that A1: E = dom (F . 0) and A2: for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ; ::_thesis: ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) set H = inferior_realsequence F; deffunc H1( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = inf (F ^\ \$1); consider G being Function such that A3: ( dom G = NAT & ( for n being Element of NAT holds G . n = H1(n) ) ) from FUNCT_1:sch_4(); now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_is_PartFunc_of_X,ExtREAL let n be Element of NAT ; ::_thesis: G . n is PartFunc of X,ExtREAL G . n = inf (F ^\ n) by A3; hence G . n is PartFunc of X,ExtREAL ; ::_thesis: verum end; then reconsider G = G as Functional_Sequence of X,ExtREAL by A3, SEQFUNC:1; A4: for n being Element of NAT holds G . n = (inferior_realsequence F) . n proof let n be Element of NAT ; ::_thesis: G . n = (inferior_realsequence F) . n (inferior_realsequence F) . n = inf (F ^\ n) by MESFUNC8:8; hence G . n = (inferior_realsequence F) . n by A3; ::_thesis: verum end; then A5: G = inferior_realsequence F by FUNCT_2:63; reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A4, FUNCT_2:63; A6: dom ((inferior_realsequence F) . 0) = dom (G . 0) by A4; A7: for n, m being Nat for x being Element of X st n <= m & x in E holds ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m ) proof let n, m be Nat; ::_thesis: for x being Element of X st n <= m & x in E holds ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m ) let x be Element of X; ::_thesis: ( n <= m & x in E implies ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m ) ) reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def_12; assume that A8: n <= m and A9: x in E ; ::_thesis: ( (G . n) . x <= (G . m) . x & (G # x) . n <= (G # x) . m ) (inferior_realsequence F) # x = inferior_realsequence (F # x) by A1, A9, MESFUNC8:7; then ((inferior_realsequence F) # x) . n1 <= ((inferior_realsequence F) # x) . m1 by A8, RINFSUP2:7; then ((inferior_realsequence F) . n) . x <= ((inferior_realsequence F) # x) . m by MESFUNC5:def_13; hence (G . n) . x <= (G . m) . x by A5, MESFUNC5:def_13; ::_thesis: (G # x) . n <= (G # x) . m then (G # x) . n <= (G . m) . x by MESFUNC5:def_13; hence (G # x) . n <= (G # x) . m by MESFUNC5:def_13; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_Element_of_X_st_x_in_E_holds_ G_#_x_is_convergent let x be Element of X; ::_thesis: ( x in E implies G # x is convergent ) assume x in E ; ::_thesis: G # x is convergent then for n, m being Element of NAT st m <= n holds (G # x) . m <= (G # x) . n by A7; then G # x is non-decreasing by RINFSUP2:7; hence G # x is convergent by RINFSUP2:37; ::_thesis: verum end; deffunc H2( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . \$1)); consider I being Function of NAT,ExtREAL such that A11: for n being Element of NAT holds I . n = H2(n) from FUNCT_2:sch_4(); A12: for n being Nat holds G . n is_measurable_on E by A1, A2, A5, MESFUNC8:20; A13: dom ((inferior_realsequence F) . 0) = dom (F . 0) by MESFUNC8:def_5; then A14: dom (lim G) = E by A1, A6, MESFUNC8:def_9; for x being set st x in dom (G . 0) holds 0 <= (G . 0) . x proof let x be set ; ::_thesis: ( x in dom (G . 0) implies 0 <= (G . 0) . x ) assume A15: x in dom (G . 0) ; ::_thesis: 0 <= (G . 0) . x then reconsider x = x as Element of X ; A16: now__::_thesis:_for_n_being_Nat_holds_0._<=_((F_#_x)_^\_0)_._n let n be Nat; ::_thesis: 0. <= ((F # x) ^\ 0) . n F . n is nonnegative by A2; then 0 <= (F . n) . x by SUPINF_2:51; then 0 <= (F # x) . (0 + n) by MESFUNC5:def_13; hence 0. <= ((F # x) ^\ 0) . n by NAT_1:def_3; ::_thesis: verum end; (F ^\ 0) . 0 = F . (0 + 0) by NAT_1:def_3; then dom (inf (F ^\ 0)) = dom (F . 0) by MESFUNC8:def_3; then (inf (F ^\ 0)) . x = inf ((F # x) ^\ 0) by A13, A6, A15, Th6; then (G . 0) . x = inf ((F # x) ^\ 0) by A3; hence 0 <= (G . 0) . x by A16, Th4; ::_thesis: verum end; then A17: G . 0 is nonnegative by SUPINF_2:52; for n, m being Nat st n <= m holds for x being Element of X st x in E holds (G . n) . x <= (G . m) . x by A7; then consider J being ExtREAL_sequence such that A18: for n being Nat holds J . n = Integral (M,(G . n)) and A19: J is convergent and A20: Integral (M,(lim G)) = lim J by A1, A13, A6, A17, A12, A10, MESFUNC9:52; reconsider I = I as ExtREAL_sequence ; for n being Nat holds J . n <= I . n proof let n be Nat; ::_thesis: J . n <= I . n A21: dom (F . n) = E by A1, MESFUNC8:def_2; A22: F . n is nonnegative by A2; A23: n is Element of NAT by ORDINAL1:def_12; A24: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(G_._n)_holds_ (G_._n)_._x_<=_(F_._n)_._x let x be Element of X; ::_thesis: ( x in dom (G . n) implies (G . n) . x <= (F . n) . x ) assume A25: x in dom (G . n) ; ::_thesis: (G . n) . x <= (F . n) . x (inferior_realsequence (F # x)) . n <= (F # x) . n by A23, RINFSUP2:8; then ((inferior_realsequence F) . n) . x <= (F # x) . n by A5, A25, MESFUNC8:def_5; then ((inferior_realsequence F) . n) . x <= (F . n) . x by MESFUNC5:def_13; hence (G . n) . x <= (F . n) . x by A4, A23; ::_thesis: verum end; A26: F . n is_measurable_on E by A2; A27: G . n is_measurable_on E by A1, A2, A5, MESFUNC8:20; A28: dom (G . n) = E by A1, A13, A6, MESFUNC8:def_2; A29: now__::_thesis:_for_x_being_set_st_x_in_dom_(G_._n)_holds_ 0_<=_(G_._n)_._x let x be set ; ::_thesis: ( x in dom (G . n) implies 0 <= (G . n) . x ) assume A30: x in dom (G . n) ; ::_thesis: 0 <= (G . n) . x 0 <= (G . 0) . x by A17, SUPINF_2:51; hence 0 <= (G . n) . x by A7, A28, A30; ::_thesis: verum end; then G . n is nonnegative by SUPINF_2:52; then integral+ (M,(G . n)) <= integral+ (M,(F . n)) by A21, A28, A26, A27, A22, A24, MESFUNC5:85; then Integral (M,(G . n)) <= integral+ (M,(F . n)) by A28, A27, A29, MESFUNC5:88, SUPINF_2:52; then A31: Integral (M,(G . n)) <= Integral (M,(F . n)) by A21, A26, A22, MESFUNC5:88; I . n = Integral (M,(F . n)) by A11, A23; hence J . n <= I . n by A18, A31; ::_thesis: verum end; then lim_inf J <= lim_inf I by Th3; then A32: lim J <= lim_inf I by A19, RINFSUP2:41; A33: dom (sup G) = E by A1, A13, A6, MESFUNC8:def_4; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_G)_holds_ (lim_G)_._x_=_(sup_G)_._x let x be Element of X; ::_thesis: ( x in dom (lim G) implies (lim G) . x = (sup G) . x ) assume A34: x in dom (lim G) ; ::_thesis: (lim G) . x = (sup G) . x then for n, m being Element of NAT st m <= n holds (G # x) . m <= (G # x) . n by A7, A14; then G # x is non-decreasing by RINFSUP2:7; then A35: lim (G # x) = sup (G # x) by RINFSUP2:37; (sup G) . x = sup (G # x) by A14, A33, A34, MESFUNC8:def_4; hence (lim G) . x = (sup G) . x by A34, A35, MESFUNC8:def_9; ::_thesis: verum end; then A36: lim G = sup G by A14, A33, PARTFUN1:5; take I ; ::_thesis: ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) for n being Nat holds I . n = Integral (M,(F . n)) proof let n be Nat; ::_thesis: I . n = Integral (M,(F . n)) n is Element of NAT by ORDINAL1:def_12; hence I . n = Integral (M,(F . n)) by A11; ::_thesis: verum end; hence ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & Integral (M,(lim_inf F)) <= lim_inf I ) by A5, A20, A36, A32, MESFUNC8:11; ::_thesis: verum end; begin theorem Th8: :: MESFUN10:8 for Y being non empty Subset of ExtREAL for r being R_eal st r in REAL holds sup ({r} + Y) = (sup {r}) + (sup Y) proof let Y be non empty Subset of ExtREAL; ::_thesis: for r being R_eal st r in REAL holds sup ({r} + Y) = (sup {r}) + (sup Y) let r be R_eal; ::_thesis: ( r in REAL implies sup ({r} + Y) = (sup {r}) + (sup Y) ) set X = {r}; assume A1: r in REAL ; ::_thesis: sup ({r} + Y) = (sup {r}) + (sup Y) set W = {r} + Y; A2: - r <> -infty by A1, XXREAL_3:23; A3: - r <> +infty by A1, XXREAL_3:23; now__::_thesis:_for_z_being_set_st_z_in_(-_{r})_+_({r}_+_Y)_holds_ z_in_Y let z be set ; ::_thesis: ( z in (- {r}) + ({r} + Y) implies z in Y ) assume z in (- {r}) + ({r} + Y) ; ::_thesis: z in Y then consider x, y being R_eal such that A4: z = x + y and A5: x in - {r} and A6: y in {r} + Y ; consider x1, y1 being R_eal such that A7: y = x1 + y1 and A8: x1 in {r} and A9: y1 in Y by A6; - x in - (- {r}) by A5; then - x in {r} ; then - x = r by TARSKI:def_1; then z = (- r) + (r + y1) by A4, A8, A7, TARSKI:def_1; then z = ((- r) + r) + y1 by A1, A3, A2, XXREAL_3:29; then z = 0. + y1 by XXREAL_3:7; hence z in Y by A9, XXREAL_3:4; ::_thesis: verum end; then A10: (- {r}) + ({r} + Y) c= Y by TARSKI:def_3; A11: r in {r} by TARSKI:def_1; now__::_thesis:_for_z_being_set_st_z_in_Y_holds_ z_in_(-_{r})_+_({r}_+_Y) let z be set ; ::_thesis: ( z in Y implies z in (- {r}) + ({r} + Y) ) assume A12: z in Y ; ::_thesis: z in (- {r}) + ({r} + Y) then reconsider y = z as Element of ExtREAL ; (r + y) - r = ((- r) + r) + y by A1, A3, A2, XXREAL_3:29; then (r + y) - r = 0. + y by XXREAL_3:7; then A13: y = (r + y) - r by XXREAL_3:4; A14: - r in - {r} by A11; r + y in {r} + Y by A11, A12; hence z in (- {r}) + ({r} + Y) by A14, A13; ::_thesis: verum end; then Y c= (- {r}) + ({r} + Y) by TARSKI:def_3; then Y = (- {r}) + ({r} + Y) by A10, XBOOLE_0:def_10; then sup Y <= (sup ({r} + Y)) + (sup (- {r})) by SUPINF_2:8; then sup Y <= (sup ({r} + Y)) + (- (inf {r})) by SUPINF_2:15; then sup Y <= (sup ({r} + Y)) - r by XXREAL_2:13; then r + (sup Y) <= sup ({r} + Y) by A1, XXREAL_3:57; then A15: (sup {r}) + (sup Y) <= sup ({r} + Y) by XXREAL_2:11; sup ({r} + Y) <= (sup {r}) + (sup Y) by SUPINF_2:8; hence sup ({r} + Y) = (sup {r}) + (sup Y) by A15, XXREAL_0:1; ::_thesis: verum end; theorem Th9: :: MESFUN10:9 for Y being non empty Subset of ExtREAL for r being R_eal st r in REAL holds inf ({r} + Y) = (inf {r}) + (inf Y) proof let Y be non empty Subset of ExtREAL; ::_thesis: for r being R_eal st r in REAL holds inf ({r} + Y) = (inf {r}) + (inf Y) let r be R_eal; ::_thesis: ( r in REAL implies inf ({r} + Y) = (inf {r}) + (inf Y) ) set X = {r}; assume A1: r in REAL ; ::_thesis: inf ({r} + Y) = (inf {r}) + (inf Y) set W = {r} + Y; set Z = - {r}; A2: - r <> -infty by A1, XXREAL_3:23; A3: - r <> +infty by A1, XXREAL_3:23; now__::_thesis:_for_z_being_set_st_z_in_(-_{r})_+_({r}_+_Y)_holds_ z_in_Y let z be set ; ::_thesis: ( z in (- {r}) + ({r} + Y) implies z in Y ) assume z in (- {r}) + ({r} + Y) ; ::_thesis: z in Y then consider x, y being R_eal such that A4: z = x + y and A5: x in - {r} and A6: y in {r} + Y ; consider x1, y1 being R_eal such that A7: y = x1 + y1 and A8: x1 in {r} and A9: y1 in Y by A6; - x in - (- {r}) by A5; then - x in {r} ; then - x = r by TARSKI:def_1; then z = (- r) + (r + y1) by A4, A8, A7, TARSKI:def_1; then z = ((- r) + r) + y1 by A1, A3, A2, XXREAL_3:29; then z = 0. + y1 by XXREAL_3:7; hence z in Y by A9, XXREAL_3:4; ::_thesis: verum end; then A10: (- {r}) + ({r} + Y) c= Y by TARSKI:def_3; A11: r in {r} by TARSKI:def_1; now__::_thesis:_for_z_being_set_st_z_in_Y_holds_ z_in_(-_{r})_+_({r}_+_Y) let z be set ; ::_thesis: ( z in Y implies z in (- {r}) + ({r} + Y) ) assume A12: z in Y ; ::_thesis: z in (- {r}) + ({r} + Y) then reconsider y = z as Element of ExtREAL ; (r + y) - r = ((- r) + r) + y by A1, A3, A2, XXREAL_3:29; then (r + y) - r = 0. + y by XXREAL_3:7; then A13: y = (r + y) - r by XXREAL_3:4; A14: - r in - {r} by A11; r + y in {r} + Y by A11, A12; hence z in (- {r}) + ({r} + Y) by A14, A13; ::_thesis: verum end; then Y c= (- {r}) + ({r} + Y) by TARSKI:def_3; then Y = (- {r}) + ({r} + Y) by A10, XBOOLE_0:def_10; then inf Y >= (inf ({r} + Y)) + (inf (- {r})) by SUPINF_2:9; then inf Y >= (inf ({r} + Y)) + (- (sup {r})) by SUPINF_2:14; then inf Y >= (inf ({r} + Y)) - r by XXREAL_2:11; then r + (inf Y) >= inf ({r} + Y) by A1, XXREAL_3:52; then A15: (inf {r}) + (inf Y) >= inf ({r} + Y) by XXREAL_2:13; inf ({r} + Y) >= (inf {r}) + (inf Y) by SUPINF_2:9; hence inf ({r} + Y) = (inf {r}) + (inf Y) by A15, XXREAL_0:1; ::_thesis: verum end; theorem Th10: :: MESFUN10:10 for seq1, seq2 being ExtREAL_sequence for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: for r being R_eal st r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) holds ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) let r be R_eal; ::_thesis: ( r in REAL & ( for n being Nat holds seq1 . n = r + (seq2 . n) ) implies ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) ) assume that A1: r in REAL and A2: for n being Nat holds seq1 . n = r + (seq2 . n) ; ::_thesis: ( lim_inf seq1 = r + (lim_inf seq2) & lim_sup seq1 = r + (lim_sup seq2) ) reconsider R1 = rng (inferior_realsequence seq1), R2 = rng (inferior_realsequence seq2), P1 = rng (superior_realsequence seq1), P2 = rng (superior_realsequence seq2) as non empty Subset of ExtREAL ; now__::_thesis:_for_z_being_set_st_z_in_{r}_+_R2_holds_ z_in_R1 let z be set ; ::_thesis: ( z in {r} + R2 implies z in R1 ) assume z in {r} + R2 ; ::_thesis: z in R1 then consider z2, z3 being R_eal such that A3: z = z2 + z3 and A4: z2 in {r} and A5: z3 in R2 ; consider n being set such that A6: n in NAT and A7: (inferior_realsequence seq2) . n = z3 by A5, FUNCT_2:11; reconsider n = n as Element of NAT by A6; consider Y2 being non empty Subset of ExtREAL such that A8: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and A9: z3 = inf Y2 by A7, RINFSUP2:def_6; consider Y1 being non empty Subset of ExtREAL such that A10: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and A11: (inferior_realsequence seq1) . n = inf Y1 by RINFSUP2:def_6; now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_ w_in_{r}_+_Y2 let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 ) A12: r in {r} by TARSKI:def_1; assume w in Y1 ; ::_thesis: w in {r} + Y2 then consider k1 being Element of NAT such that A13: w = seq1 . k1 and A14: n <= k1 by A10; reconsider w1 = w as R_eal by A13; A15: seq2 . k1 in Y2 by A8, A14; w1 = r + (seq2 . k1) by A2, A13; hence w in {r} + Y2 by A12, A15; ::_thesis: verum end; then A16: Y1 c= {r} + Y2 by TARSKI:def_3; now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_ w_in_Y1 let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 ) assume w in {r} + Y2 ; ::_thesis: w in Y1 then consider w1, w2 being R_eal such that A17: w = w1 + w2 and A18: w1 in {r} and A19: w2 in Y2 ; consider k2 being Element of NAT such that A20: w2 = seq2 . k2 and A21: n <= k2 by A8, A19; w1 = r by A18, TARSKI:def_1; then w = seq1 . k2 by A2, A17, A20; hence w in Y1 by A10, A21; ::_thesis: verum end; then {r} + Y2 c= Y1 by TARSKI:def_3; then Y1 = {r} + Y2 by A16, XBOOLE_0:def_10; then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9; then inf Y1 = r + (inf Y2) by XXREAL_2:13; then z = (inferior_realsequence seq1) . n by A4, A3, A9, A11, TARSKI:def_1; hence z in R1 by FUNCT_2:4; ::_thesis: verum end; then A22: {r} + R2 c= R1 by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_{r}_+_P2_holds_ z_in_P1 let z be set ; ::_thesis: ( z in {r} + P2 implies z in P1 ) assume z in {r} + P2 ; ::_thesis: z in P1 then consider z2, z3 being R_eal such that A23: z = z2 + z3 and A24: z2 in {r} and A25: z3 in P2 ; consider n being set such that A26: n in NAT and A27: (superior_realsequence seq2) . n = z3 by A25, FUNCT_2:11; reconsider n = n as Element of NAT by A26; consider Y2 being non empty Subset of ExtREAL such that A28: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and A29: z3 = sup Y2 by A27, RINFSUP2:def_7; consider Y1 being non empty Subset of ExtREAL such that A30: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and A31: (superior_realsequence seq1) . n = sup Y1 by RINFSUP2:def_7; now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_ w_in_{r}_+_Y2 let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 ) A32: r in {r} by TARSKI:def_1; assume w in Y1 ; ::_thesis: w in {r} + Y2 then consider k1 being Element of NAT such that A33: w = seq1 . k1 and A34: n <= k1 by A30; reconsider w1 = w as R_eal by A33; A35: seq2 . k1 in Y2 by A28, A34; w1 = r + (seq2 . k1) by A2, A33; hence w in {r} + Y2 by A32, A35; ::_thesis: verum end; then A36: Y1 c= {r} + Y2 by TARSKI:def_3; now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_ w_in_Y1 let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 ) assume w in {r} + Y2 ; ::_thesis: w in Y1 then consider w1, w2 being R_eal such that A37: w = w1 + w2 and A38: w1 in {r} and A39: w2 in Y2 ; consider k2 being Element of NAT such that A40: w2 = seq2 . k2 and A41: n <= k2 by A28, A39; w1 = r by A38, TARSKI:def_1; then w = seq1 . k2 by A2, A37, A40; hence w in Y1 by A30, A41; ::_thesis: verum end; then {r} + Y2 c= Y1 by TARSKI:def_3; then Y1 = {r} + Y2 by A36, XBOOLE_0:def_10; then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8; then sup Y1 = r + (sup Y2) by XXREAL_2:11; then z = (superior_realsequence seq1) . n by A24, A23, A29, A31, TARSKI:def_1; hence z in P1 by FUNCT_2:4; ::_thesis: verum end; then A42: {r} + P2 c= P1 by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_R1_holds_ z_in_{r}_+_R2 let z be set ; ::_thesis: ( z in R1 implies z in {r} + R2 ) assume z in R1 ; ::_thesis: z in {r} + R2 then consider n being set such that A43: n in NAT and A44: (inferior_realsequence seq1) . n = z by FUNCT_2:11; reconsider n = n as Element of NAT by A43; consider Y1 being non empty Subset of ExtREAL such that A45: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and A46: z = inf Y1 by A44, RINFSUP2:def_6; consider Y2 being non empty Subset of ExtREAL such that A47: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and A48: (inferior_realsequence seq2) . n = inf Y2 by RINFSUP2:def_6; now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_ w_in_{r}_+_Y2 let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 ) A49: r in {r} by TARSKI:def_1; assume w in Y1 ; ::_thesis: w in {r} + Y2 then consider k1 being Element of NAT such that A50: w = seq1 . k1 and A51: n <= k1 by A45; reconsider w1 = w as R_eal by A50; A52: seq2 . k1 in Y2 by A47, A51; w1 = r + (seq2 . k1) by A2, A50; hence w in {r} + Y2 by A49, A52; ::_thesis: verum end; then A53: Y1 c= {r} + Y2 by TARSKI:def_3; now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_ w_in_Y1 let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 ) assume w in {r} + Y2 ; ::_thesis: w in Y1 then consider w1, w2 being R_eal such that A54: w = w1 + w2 and A55: w1 in {r} and A56: w2 in Y2 ; consider k2 being Element of NAT such that A57: w2 = seq2 . k2 and A58: n <= k2 by A47, A56; w1 = r by A55, TARSKI:def_1; then w = seq1 . k2 by A2, A54, A57; hence w in Y1 by A45, A58; ::_thesis: verum end; then {r} + Y2 c= Y1 by TARSKI:def_3; then Y1 = {r} + Y2 by A53, XBOOLE_0:def_10; then inf Y1 = (inf {r}) + (inf Y2) by A1, Th9; then A59: inf Y1 = r + (inf Y2) by XXREAL_2:13; A60: (inferior_realsequence seq2) . n in R2 by FUNCT_2:4; r in {r} by TARSKI:def_1; hence z in {r} + R2 by A46, A48, A59, A60; ::_thesis: verum end; then R1 c= {r} + R2 by TARSKI:def_3; then R1 = {r} + R2 by A22, XBOOLE_0:def_10; then sup R1 = (sup {r}) + (sup R2) by A1, Th8; hence lim_inf seq1 = r + (lim_inf seq2) by XXREAL_2:11; ::_thesis: lim_sup seq1 = r + (lim_sup seq2) now__::_thesis:_for_z_being_set_st_z_in_P1_holds_ z_in_{r}_+_P2 let z be set ; ::_thesis: ( z in P1 implies z in {r} + P2 ) assume z in P1 ; ::_thesis: z in {r} + P2 then consider n being set such that A61: n in NAT and A62: (superior_realsequence seq1) . n = z by FUNCT_2:11; reconsider n = n as Element of NAT by A61; consider Y1 being non empty Subset of ExtREAL such that A63: Y1 = { (seq1 . k) where k is Element of NAT : n <= k } and A64: z = sup Y1 by A62, RINFSUP2:def_7; consider Y2 being non empty Subset of ExtREAL such that A65: Y2 = { (seq2 . k) where k is Element of NAT : n <= k } and A66: (superior_realsequence seq2) . n = sup Y2 by RINFSUP2:def_7; now__::_thesis:_for_w_being_set_st_w_in_Y1_holds_ w_in_{r}_+_Y2 let w be set ; ::_thesis: ( w in Y1 implies w in {r} + Y2 ) A67: r in {r} by TARSKI:def_1; assume w in Y1 ; ::_thesis: w in {r} + Y2 then consider k1 being Element of NAT such that A68: w = seq1 . k1 and A69: n <= k1 by A63; reconsider w1 = w as R_eal by A68; A70: seq2 . k1 in Y2 by A65, A69; w1 = r + (seq2 . k1) by A2, A68; hence w in {r} + Y2 by A67, A70; ::_thesis: verum end; then A71: Y1 c= {r} + Y2 by TARSKI:def_3; now__::_thesis:_for_w_being_set_st_w_in_{r}_+_Y2_holds_ w_in_Y1 let w be set ; ::_thesis: ( w in {r} + Y2 implies w in Y1 ) assume w in {r} + Y2 ; ::_thesis: w in Y1 then consider w1, w2 being R_eal such that A72: w = w1 + w2 and A73: w1 in {r} and A74: w2 in Y2 ; consider k2 being Element of NAT such that A75: w2 = seq2 . k2 and A76: n <= k2 by A65, A74; w1 = r by A73, TARSKI:def_1; then w = seq1 . k2 by A2, A72, A75; hence w in Y1 by A63, A76; ::_thesis: verum end; then {r} + Y2 c= Y1 by TARSKI:def_3; then Y1 = {r} + Y2 by A71, XBOOLE_0:def_10; then sup Y1 = (sup {r}) + (sup Y2) by A1, Th8; then A77: sup Y1 = r + (sup Y2) by XXREAL_2:11; A78: (superior_realsequence seq2) . n in P2 by FUNCT_2:4; r in {r} by TARSKI:def_1; hence z in {r} + P2 by A64, A66, A77, A78; ::_thesis: verum end; then P1 c= {r} + P2 by TARSKI:def_3; then P1 = {r} + P2 by A42, XBOOLE_0:def_10; then inf P1 = (inf {r}) + (inf P2) by A1, Th9; hence lim_sup seq1 = r + (lim_sup seq2) by XXREAL_2:13; ::_thesis: verum end; theorem Th11: :: MESFUN10:11 for X being non empty set for F1, F2 being Functional_Sequence of X,ExtREAL for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) proof let X be non empty set ; ::_thesis: for F1, F2 being Functional_Sequence of X,ExtREAL for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) let F1, F2 be Functional_Sequence of X,ExtREAL; ::_thesis: for f being PartFunc of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) holds ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & f " {+infty} = {} & f " {-infty} = {} & ( for n being Nat holds F1 . n = f + (F2 . n) ) implies ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) ) assume that A1: dom (F1 . 0) = dom (F2 . 0) and A2: F1 is with_the_same_dom and A3: f " {+infty} = {} and A4: f " {-infty} = {} and A5: for n being Nat holds F1 . n = f + (F2 . n) ; ::_thesis: ( lim_inf F1 = f + (lim_inf F2) & lim_sup F1 = f + (lim_sup F2) ) A6: F1 . 0 = f + (F2 . 0) by A5; A7: dom (f + (F2 . 0)) = ((dom f) /\ (dom (F2 . 0))) \ (((f " {-infty}) /\ ((F2 . 0) " {+infty})) \/ ((f " {+infty}) /\ ((F2 . 0) " {-infty}))) by MESFUNC1:def_3; A8: dom (f + (lim_sup F2)) = ((dom f) /\ (dom (lim_sup F2))) \ (((f " {-infty}) /\ ((lim_sup F2) " {+infty})) \/ ((f " {+infty}) /\ ((lim_sup F2) " {-infty}))) by MESFUNC1:def_3; then A9: dom (f + (lim_sup F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def_8; then A10: dom (lim_sup F1) = dom (f + (lim_sup F2)) by A3, A4, A6, A7, MESFUNC8:def_8; A11: dom (f + (lim_inf F2)) = ((dom f) /\ (dom (lim_inf F2))) \ (((f " {-infty}) /\ ((lim_inf F2) " {+infty})) \/ ((f " {+infty}) /\ ((lim_inf F2) " {-infty}))) by MESFUNC1:def_3; then A12: dom (f + (lim_inf F2)) = (dom f) /\ (dom (F2 . 0)) by A3, A4, MESFUNC8:def_7; then A13: dom (lim_inf F1) = dom (f + (lim_inf F2)) by A3, A4, A6, A7, MESFUNC8:def_7; A14: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def_7; A15: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def_7; for x being Element of X st x in dom (lim_inf F1) holds (lim_inf F1) . x = (f + (lim_inf F2)) . x proof let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (f + (lim_inf F2)) . x ) assume A16: x in dom (lim_inf F1) ; ::_thesis: (lim_inf F1) . x = (f + (lim_inf F2)) . x then A17: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def_7; A18: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n) proof let n be Nat; ::_thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n) F1 . n = f + (F2 . n) by A5; then dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def_2; then A19: x in dom (f + (F2 . n)) by A16, MESFUNC8:def_7; (F1 . n) . x = (f + (F2 . n)) . x by A5; then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A19, MESFUNC1:def_3; then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def_13; hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def_13; ::_thesis: verum end; A20: dom (f + (lim_inf F2)) c= dom f by A3, A4, A11, XBOOLE_1:17; then not f . x in {-infty} by A4, A13, A16, FUNCT_1:def_7; then A21: f . x <> -infty by TARSKI:def_1; not f . x in {+infty} by A3, A13, A16, A20, FUNCT_1:def_7; then f . x <> +infty by TARSKI:def_1; then A22: f . x is Real by A21, XXREAL_0:14; x in dom (f + (lim_inf F2)) by A3, A4, A6, A7, A12, A16, MESFUNC8:def_7; then A23: (f + (lim_inf F2)) . x = (f . x) + ((lim_inf F2) . x) by MESFUNC1:def_3; (lim_inf F2) . x = lim_inf (F2 # x) by A1, A15, A14, A16, MESFUNC8:def_7; hence (lim_inf F1) . x = (f + (lim_inf F2)) . x by A22, A18, A17, A23, Th10; ::_thesis: verum end; hence lim_inf F1 = f + (lim_inf F2) by A13, PARTFUN1:5; ::_thesis: lim_sup F1 = f + (lim_sup F2) A24: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def_8; A25: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def_8; for x being Element of X st x in dom (lim_sup F1) holds (lim_sup F1) . x = (f + (lim_sup F2)) . x proof let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (f + (lim_sup F2)) . x ) assume A26: x in dom (lim_sup F1) ; ::_thesis: (lim_sup F1) . x = (f + (lim_sup F2)) . x then A27: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def_8; A28: for n being Nat holds (F1 # x) . n = (f . x) + ((F2 # x) . n) proof let n be Nat; ::_thesis: (F1 # x) . n = (f . x) + ((F2 # x) . n) F1 . n = f + (F2 . n) by A5; then A29: dom (f + (F2 . n)) = dom (F1 . 0) by A2, MESFUNC8:def_2; (F1 . n) . x = (f + (F2 . n)) . x by A5; then (F1 . n) . x = (f . x) + ((F2 . n) . x) by A24, A26, A29, MESFUNC1:def_3; then (F1 # x) . n = (f . x) + ((F2 . n) . x) by MESFUNC5:def_13; hence (F1 # x) . n = (f . x) + ((F2 # x) . n) by MESFUNC5:def_13; ::_thesis: verum end; A30: dom (f + (lim_sup F2)) c= dom f by A3, A4, A8, XBOOLE_1:17; then not f . x in {-infty} by A4, A10, A26, FUNCT_1:def_7; then A31: f . x <> -infty by TARSKI:def_1; not f . x in {+infty} by A3, A10, A26, A30, FUNCT_1:def_7; then f . x <> +infty by TARSKI:def_1; then A32: f . x is Real by A31, XXREAL_0:14; x in dom (f + (lim_sup F2)) by A3, A4, A6, A7, A9, A26, MESFUNC8:def_8; then A33: (f + (lim_sup F2)) . x = (f . x) + ((lim_sup F2) . x) by MESFUNC1:def_3; (lim_sup F2) . x = lim_sup (F2 # x) by A1, A24, A25, A26, MESFUNC8:def_8; hence (lim_sup F1) . x = (f + (lim_sup F2)) . x by A32, A28, A27, A33, Th10; ::_thesis: verum end; hence lim_sup F1 = f + (lim_sup F2) by A10, PARTFUN1:5; ::_thesis: verum end; theorem Th12: :: MESFUN10:12 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds f - g is_integrable_on M proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds f - g is_integrable_on M let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds f - g is_integrable_on M let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds f - g is_integrable_on M let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies f - g is_integrable_on M ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: f - g is_integrable_on M (- 1) (#) g is_integrable_on M by A2, MESFUNC5:110; then - g is_integrable_on M by MESFUNC2:9; then f + (- g) is_integrable_on M by A1, MESFUNC5:108; hence f - g is_integrable_on M by MESFUNC2:8; ::_thesis: verum end; theorem Th13: :: MESFUN10:13 for X being non empty set for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) let M be sigma_Measure of S; ::_thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) let f, g be PartFunc of X,ExtREAL; ::_thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) ) assume that A1: f is_integrable_on M and A2: g is_integrable_on M ; ::_thesis: ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) (- 1) (#) g is_integrable_on M by A2, MESFUNC5:110; then - g is_integrable_on M by MESFUNC2:9; then consider E being Element of S such that A3: E = (dom f) /\ (dom (- g)) and A4: Integral (M,(f + (- g))) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) by A1, MESFUNC5:109; A5: dom g = dom (- g) by MESFUNC1:def_7; Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) by A4, MESFUNC2:8; hence ex E being Element of S st ( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) by A3, A5; ::_thesis: verum end; theorem Th14: :: MESFUN10:14 for seq1, seq2 being ExtREAL_sequence st ( for n being Nat holds seq1 . n = - (seq2 . n) ) holds ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) ) proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Nat holds seq1 . n = - (seq2 . n) ) implies ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) ) ) assume A1: for n being Nat holds seq1 . n = - (seq2 . n) ; ::_thesis: ( lim_inf seq2 = - (lim_sup seq1) & lim_sup seq2 = - (lim_inf seq1) ) now__::_thesis:_for_z_being_set_st_z_in_rng_(inferior_realsequence_seq2)_holds_ z_in_-_(rng_(superior_realsequence_seq1)) let z be set ; ::_thesis: ( z in rng (inferior_realsequence seq2) implies z in - (rng (superior_realsequence seq1)) ) assume z in rng (inferior_realsequence seq2) ; ::_thesis: z in - (rng (superior_realsequence seq1)) then consider n being set such that A2: n in dom (inferior_realsequence seq2) and A3: z = (inferior_realsequence seq2) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A2; consider R2 being non empty Subset of ExtREAL such that A4: R2 = { (seq2 . k) where k is Element of NAT : n <= k } and A5: z = inf R2 by A3, RINFSUP2:def_6; reconsider z2 = z as Element of ExtREAL by A3; set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ; reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5; set z1 = - z2; A6: ex K1 being non empty Subset of ExtREAL st ( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq1) . n = sup K1 ) by RINFSUP2:def_7; now__::_thesis:_for_x_being_set_st_x_in_R1_holds_ x_in_-_R2 let x be set ; ::_thesis: ( x in R1 implies x in - R2 ) assume x in R1 ; ::_thesis: x in - R2 then consider k being Element of NAT such that A7: x = seq1 . k and A8: n <= k ; reconsider x1 = x as Element of ExtREAL by A7; - x1 = - (- (seq2 . k)) by A1, A7; then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by A8; then - (- x1) in - R2 by A4; hence x in - R2 ; ::_thesis: verum end; then A9: R1 c= - R2 by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_-_R2_holds_ x_in_R1 let x be set ; ::_thesis: ( x in - R2 implies x in R1 ) assume x in - R2 ; ::_thesis: x in R1 then consider y being R_eal such that A10: x = - y and A11: y in R2 ; consider k being Element of NAT such that A12: y = seq2 . k and A13: n <= k by A4, A11; seq1 . k = - (seq2 . k) by A1; hence x in R1 by A10, A12, A13; ::_thesis: verum end; then - R2 c= R1 by TARSKI:def_3; then - R2 = R1 by A9, XBOOLE_0:def_10; then (superior_realsequence seq1) . n = - z2 by A5, A6, SUPINF_2:15; then A14: - z2 in rng (superior_realsequence seq1) by FUNCT_2:4; z2 = - (- z2) ; hence z in - (rng (superior_realsequence seq1)) by A14; ::_thesis: verum end; then A15: rng (inferior_realsequence seq2) c= - (rng (superior_realsequence seq1)) by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_rng_(superior_realsequence_seq2)_holds_ z_in_-_(rng_(inferior_realsequence_seq1)) let z be set ; ::_thesis: ( z in rng (superior_realsequence seq2) implies z in - (rng (inferior_realsequence seq1)) ) assume z in rng (superior_realsequence seq2) ; ::_thesis: z in - (rng (inferior_realsequence seq1)) then consider n being set such that A16: n in dom (superior_realsequence seq2) and A17: z = (superior_realsequence seq2) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A16; consider R2 being non empty Subset of ExtREAL such that A18: R2 = { (seq2 . k) where k is Element of NAT : n <= k } and A19: z = sup R2 by A17, RINFSUP2:def_7; reconsider z2 = z as Element of ExtREAL by A17; set R1 = { (seq1 . k) where k is Element of NAT : n <= k } ; reconsider R1 = { (seq1 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5; set z1 = - z2; A20: ex K1 being non empty Subset of ExtREAL st ( K1 = { (seq1 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq1) . n = inf K1 ) by RINFSUP2:def_6; now__::_thesis:_for_x_being_set_st_x_in_R1_holds_ x_in_-_R2 let x be set ; ::_thesis: ( x in R1 implies x in - R2 ) assume x in R1 ; ::_thesis: x in - R2 then consider k being Element of NAT such that A21: x = seq1 . k and A22: n <= k ; reconsider x1 = x as Element of ExtREAL by A21; - x1 = - (- (seq2 . k)) by A1, A21; then - x1 in { (seq2 . k2) where k2 is Element of NAT : n <= k2 } by A22; then - (- x1) in - R2 by A18; hence x in - R2 ; ::_thesis: verum end; then A23: R1 c= - R2 by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_-_R2_holds_ x_in_R1 let x be set ; ::_thesis: ( x in - R2 implies x in R1 ) assume x in - R2 ; ::_thesis: x in R1 then consider y being R_eal such that A24: x = - y and A25: y in R2 ; consider k being Element of NAT such that A26: y = seq2 . k and A27: n <= k by A18, A25; seq1 . k = - (seq2 . k) by A1; hence x in R1 by A24, A26, A27; ::_thesis: verum end; then - R2 c= R1 by TARSKI:def_3; then - R2 = R1 by A23, XBOOLE_0:def_10; then (inferior_realsequence seq1) . n = - z2 by A19, A20, SUPINF_2:14; then A28: - z2 in rng (inferior_realsequence seq1) by FUNCT_2:4; z2 = - (- z2) ; hence z in - (rng (inferior_realsequence seq1)) by A28; ::_thesis: verum end; then A29: rng (superior_realsequence seq2) c= - (rng (inferior_realsequence seq1)) by TARSKI:def_3; now__::_thesis:_for_z_being_set_st_z_in_-_(rng_(superior_realsequence_seq1))_holds_ z_in_rng_(inferior_realsequence_seq2) let z be set ; ::_thesis: ( z in - (rng (superior_realsequence seq1)) implies z in rng (inferior_realsequence seq2) ) assume z in - (rng (superior_realsequence seq1)) ; ::_thesis: z in rng (inferior_realsequence seq2) then consider t being R_eal such that A30: z = - t and A31: t in rng (superior_realsequence seq1) ; consider n being set such that A32: n in dom (superior_realsequence seq1) and A33: t = (superior_realsequence seq1) . n by A31, FUNCT_1:def_3; reconsider n = n as Element of NAT by A32; consider R1 being non empty Subset of ExtREAL such that A34: R1 = { (seq1 . k) where k is Element of NAT : n <= k } and A35: t = sup R1 by A33, RINFSUP2:def_7; reconsider z1 = z as Element of ExtREAL by A30; set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ; reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5; A36: ex K2 being non empty Subset of ExtREAL st ( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq2) . n = inf K2 ) by RINFSUP2:def_6; now__::_thesis:_for_x_being_set_st_x_in_R2_holds_ x_in_-_R1 let x be set ; ::_thesis: ( x in R2 implies x in - R1 ) assume x in R2 ; ::_thesis: x in - R1 then consider k being Element of NAT such that A37: x = seq2 . k and A38: n <= k ; reconsider x1 = x as Element of ExtREAL by A37; - x1 = - (- (seq1 . k)) by A1, A37; then - x1 in { (seq1 . k2) where k2 is Element of NAT : n <= k2 } by A38; then - (- x1) in - R1 by A34; hence x in - R1 ; ::_thesis: verum end; then A39: R2 c= - R1 by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_-_R1_holds_ x_in_R2 let x be set ; ::_thesis: ( x in - R1 implies x in R2 ) assume x in - R1 ; ::_thesis: x in R2 then consider y being R_eal such that A40: x = - y and A41: y in R1 ; consider k being Element of NAT such that A42: y = seq1 . k and A43: n <= k by A34, A41; seq1 . k = - (seq2 . k) by A1; hence x in R2 by A40, A42, A43; ::_thesis: verum end; then - R1 c= R2 by TARSKI:def_3; then - R1 = R2 by A39, XBOOLE_0:def_10; then (inferior_realsequence seq2) . n = z1 by A30, A35, A36, SUPINF_2:14; hence z in rng (inferior_realsequence seq2) by FUNCT_2:4; ::_thesis: verum end; then - (rng (superior_realsequence seq1)) c= rng (inferior_realsequence seq2) by TARSKI:def_3; then rng (inferior_realsequence seq2) = - (rng (superior_realsequence seq1)) by A15, XBOOLE_0:def_10; hence lim_inf seq2 = - (lim_sup seq1) by SUPINF_2:15; ::_thesis: lim_sup seq2 = - (lim_inf seq1) now__::_thesis:_for_z_being_set_st_z_in_-_(rng_(inferior_realsequence_seq1))_holds_ z_in_rng_(superior_realsequence_seq2) let z be set ; ::_thesis: ( z in - (rng (inferior_realsequence seq1)) implies z in rng (superior_realsequence seq2) ) assume z in - (rng (inferior_realsequence seq1)) ; ::_thesis: z in rng (superior_realsequence seq2) then consider t being R_eal such that A44: z = - t and A45: t in rng (inferior_realsequence seq1) ; consider n being set such that A46: n in dom (inferior_realsequence seq1) and A47: t = (inferior_realsequence seq1) . n by A45, FUNCT_1:def_3; reconsider n = n as Element of NAT by A46; consider R1 being non empty Subset of ExtREAL such that A48: R1 = { (seq1 . k) where k is Element of NAT : n <= k } and A49: t = inf R1 by A47, RINFSUP2:def_6; reconsider z1 = z as Element of ExtREAL by A44; set R2 = { (seq2 . k) where k is Element of NAT : n <= k } ; reconsider R2 = { (seq2 . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by RINFSUP2:5; A50: ex K2 being non empty Subset of ExtREAL st ( K2 = { (seq2 . k) where k is Element of NAT : n <= k } & (superior_realsequence seq2) . n = sup K2 ) by RINFSUP2:def_7; now__::_thesis:_for_x_being_set_st_x_in_R2_holds_ x_in_-_R1 let x be set ; ::_thesis: ( x in R2 implies x in - R1 ) assume x in R2 ; ::_thesis: x in - R1 then consider k being Element of NAT such that A51: x = seq2 . k and A52: n <= k ; reconsider x1 = x as Element of ExtREAL by A51; seq1 . k = - (seq2 . k) by A1; then - x1 in R1 by A48, A51, A52; then - (- x1) in - R1 ; hence x in - R1 ; ::_thesis: verum end; then A53: R2 c= - R1 by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_-_R1_holds_ x_in_R2 let x be set ; ::_thesis: ( x in - R1 implies x in R2 ) assume x in - R1 ; ::_thesis: x in R2 then consider y being R_eal such that A54: x = - y and A55: y in R1 ; consider k being Element of NAT such that A56: y = seq1 . k and A57: n <= k by A48, A55; seq1 . k = - (seq2 . k) by A1; hence x in R2 by A54, A56, A57; ::_thesis: verum end; then - R1 c= R2 by TARSKI:def_3; then - R1 = R2 by A53, XBOOLE_0:def_10; then (superior_realsequence seq2) . n = z1 by A44, A49, A50, SUPINF_2:15; hence z in rng (superior_realsequence seq2) by FUNCT_2:4; ::_thesis: verum end; then - (rng (inferior_realsequence seq1)) c= rng (superior_realsequence seq2) by TARSKI:def_3; then rng (superior_realsequence seq2) = - (rng (inferior_realsequence seq1)) by A29, XBOOLE_0:def_10; hence lim_sup seq2 = - (lim_inf seq1) by SUPINF_2:14; ::_thesis: verum end; theorem Th15: :: MESFUN10:15 for X being non empty set for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) proof let X be non empty set ; ::_thesis: for F1, F2 being Functional_Sequence of X,ExtREAL st dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) holds ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) let F1, F2 be Functional_Sequence of X,ExtREAL; ::_thesis: ( dom (F1 . 0) = dom (F2 . 0) & F1 is with_the_same_dom & ( for n being Nat holds F1 . n = - (F2 . n) ) implies ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) ) assume that A1: dom (F1 . 0) = dom (F2 . 0) and A2: F1 is with_the_same_dom and A3: for n being Nat holds F1 . n = - (F2 . n) ; ::_thesis: ( lim_inf F1 = - (lim_sup F2) & lim_sup F1 = - (lim_inf F2) ) A4: dom (lim_inf F1) = dom (F1 . 0) by MESFUNC8:def_7; A5: dom (lim_sup F2) = dom (F2 . 0) by MESFUNC8:def_8; A6: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F1_._0)_holds_ for_n_being_Nat_holds_(F2_#_x)_._n_=_-_((F1_#_x)_._n) let x be Element of X; ::_thesis: ( x in dom (F1 . 0) implies for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) ) assume A7: x in dom (F1 . 0) ; ::_thesis: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) let n be Nat; ::_thesis: (F2 # x) . n = - ((F1 # x) . n) dom (F1 . n) = dom (F1 . 0) by A2, MESFUNC8:def_2; then A8: x in dom (- (F2 . n)) by A3, A7; (F1 . n) . x = (- (F2 . n)) . x by A3; then (F1 . n) . x = - ((F2 . n) . x) by A8, MESFUNC1:def_7; then (F1 # x) . n = - ((F2 . n) . x) by MESFUNC5:def_13; hence (F2 # x) . n = - ((F1 # x) . n) by MESFUNC5:def_13; ::_thesis: verum end; A9: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F1)_holds_ (lim_inf_F1)_._x_=_(-_(lim_sup_F2))_._x let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies (lim_inf F1) . x = (- (lim_sup F2)) . x ) assume A10: x in dom (lim_inf F1) ; ::_thesis: (lim_inf F1) . x = (- (lim_sup F2)) . x then A11: (lim_inf F1) . x = lim_inf (F1 # x) by MESFUNC8:def_7; x in dom (- (lim_sup F2)) by A1, A4, A5, A10, MESFUNC1:def_7; then A12: (- (lim_sup F2)) . x = - ((lim_sup F2) . x) by MESFUNC1:def_7; A13: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A4, A6, A10; (lim_sup F2) . x = lim_sup (F2 # x) by A1, A4, A5, A10, MESFUNC8:def_8; hence (lim_inf F1) . x = (- (lim_sup F2)) . x by A13, A11, A12, Th14; ::_thesis: verum end; dom (- (lim_sup F2)) = dom (lim_sup F2) by MESFUNC1:def_7; hence lim_inf F1 = - (lim_sup F2) by A1, A4, A5, A9, PARTFUN1:5; ::_thesis: lim_sup F1 = - (lim_inf F2) A14: dom (lim_sup F1) = dom (F1 . 0) by MESFUNC8:def_8; A15: dom (lim_inf F2) = dom (F2 . 0) by MESFUNC8:def_7; A16: for x being Element of X st x in dom (lim_sup F1) holds (lim_sup F1) . x = (- (lim_inf F2)) . x proof let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies (lim_sup F1) . x = (- (lim_inf F2)) . x ) assume A17: x in dom (lim_sup F1) ; ::_thesis: (lim_sup F1) . x = (- (lim_inf F2)) . x then A18: (lim_sup F1) . x = lim_sup (F1 # x) by MESFUNC8:def_8; x in dom (- (lim_inf F2)) by A1, A14, A15, A17, MESFUNC1:def_7; then A19: (- (lim_inf F2)) . x = - ((lim_inf F2) . x) by MESFUNC1:def_7; A20: for n being Nat holds (F2 # x) . n = - ((F1 # x) . n) by A14, A6, A17; (lim_inf F2) . x = lim_inf (F2 # x) by A1, A14, A15, A17, MESFUNC8:def_7; hence (lim_sup F1) . x = (- (lim_inf F2)) . x by A20, A18, A19, Th14; ::_thesis: verum end; dom (- (lim_inf F2)) = dom (lim_inf F2) by MESFUNC1:def_7; hence lim_sup F1 = - (lim_inf F2) by A1, A14, A15, A16, PARTFUN1:5; ::_thesis: verum end; theorem Th16: :: MESFUN10:16 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let M be sigma_Measure of S; ::_thesis: for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) implies ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) ) assume that A1: E = dom (F . 0) and A2: E = dom P and A3: for n being Nat holds F . n is_measurable_on E and A4: P is_integrable_on M and A5: for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ; ::_thesis: ( ( for n being Nat holds |.(F . n).| is_integrable_on M ) & |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) A6: lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24; hereby ::_thesis: ( |.(lim_inf F).| is_integrable_on M & |.(lim_sup F).| is_integrable_on M ) let n be Nat; ::_thesis: |.(F . n).| is_integrable_on M A7: F . n is_measurable_on E by A3; A8: E = dom (F . n) by A1, MESFUNC8:def_2; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_ |.((F_._n)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (F . n) implies |.((F . n) . x).| <= P . x ) assume A9: x in dom (F . n) ; ::_thesis: |.((F . n) . x).| <= P . x then A10: x in dom |.(F . n).| by MESFUNC1:def_10; |.(F . n).| . x <= P . x by A5, A8, A9; hence |.((F . n) . x).| <= P . x by A10, MESFUNC1:def_10; ::_thesis: verum end; then F . n is_integrable_on M by A2, A4, A8, A7, MESFUNC5:102; hence |.(F . n).| is_integrable_on M by A8, A7, MESFUNC5:100; ::_thesis: verum end; A11: E = dom (lim_inf F) by A1, MESFUNC8:def_7; A12: lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23; A13: for x being Element of X for k being Nat st x in E holds ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) proof let x be Element of X; ::_thesis: for k being Nat st x in E holds ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) let k be Nat; ::_thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) ) assume A14: x in E ; ::_thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) then x in dom (F . k) by A1, MESFUNC8:def_2; then A15: x in dom |.(F . k).| by MESFUNC1:def_10; |.(F . k).| . x <= P . x by A5, A14; then A16: |.((F . k) . x).| <= P . x by A15, MESFUNC1:def_10; then A17: (F . k) . x <= P . x by EXTREAL2:12; - (P . x) <= (F . k) . x by A16, EXTREAL2:12; hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A17, MESFUNC5:def_13; ::_thesis: verum end; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F)_holds_ |.((lim_inf_F)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (lim_inf F) implies |.((lim_inf F) . x).| <= P . x ) assume A18: x in dom (lim_inf F) ; ::_thesis: |.((lim_inf F) . x).| <= P . x then A19: x in E by A1, MESFUNC8:def_7; for k being Nat holds (inferior_realsequence (F # x)) . k <= P . x proof let k be Nat; ::_thesis: (inferior_realsequence (F # x)) . k <= P . x reconsider k1 = k as Element of NAT by ORDINAL1:def_12; A20: (inferior_realsequence (F # x)) . k1 <= (F # x) . k1 by RINFSUP2:8; (F # x) . k <= P . x by A13, A19; hence (inferior_realsequence (F # x)) . k <= P . x by A20, XXREAL_0:2; ::_thesis: verum end; then lim_inf (F # x) <= P . x by Th5; then A21: (lim_inf F) . x <= P . x by A18, MESFUNC8:def_7; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_ -_(P_._x)_<=_y let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies - (P . x) <= y ) assume y in rng (F # x) ; ::_thesis: - (P . x) <= y then ex k being set st ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3; hence - (P . x) <= y by A13, A19; ::_thesis: verum end; then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def_2; then - (P . x) <= inf (F # x) by XXREAL_2:def_4; then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47; then A22: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27; (inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23; then - (P . x) <= lim_inf (F # x) by A22, XXREAL_0:2; then - (P . x) <= (lim_inf F) . x by A18, MESFUNC8:def_7; hence |.((lim_inf F) . x).| <= P . x by A21, EXTREAL2:12; ::_thesis: verum end; then lim_inf F is_integrable_on M by A2, A4, A11, A6, MESFUNC5:102; hence |.(lim_inf F).| is_integrable_on M by A11, A6, MESFUNC5:100; ::_thesis: |.(lim_sup F).| is_integrable_on M A23: E = dom (lim_sup F) by A1, MESFUNC8:def_8; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F)_holds_ |.((lim_sup_F)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x ) assume A24: x in dom (lim_sup F) ; ::_thesis: |.((lim_sup F) . x).| <= P . x for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x) proof let k be Nat; ::_thesis: (superior_realsequence (F # x)) . k >= - (P . x) reconsider k1 = k as Element of NAT by ORDINAL1:def_12; A25: (superior_realsequence (F # x)) . k1 >= (F # x) . k1 by RINFSUP2:8; (F # x) . k >= - (P . x) by A23, A13, A24; hence (superior_realsequence (F # x)) . k >= - (P . x) by A25, XXREAL_0:2; ::_thesis: verum end; then lim_sup (F # x) >= - (P . x) by Th4; then A26: (lim_sup F) . x >= - (P . x) by A24, MESFUNC8:def_8; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_ P_._x_>=_y let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies P . x >= y ) assume y in rng (F # x) ; ::_thesis: P . x >= y then ex k being set st ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3; hence P . x >= y by A23, A13, A24; ::_thesis: verum end; then P . x is UpperBound of rng (F # x) by XXREAL_2:def_1; then P . x >= sup (rng (F # x)) by XXREAL_2:def_3; then P . x >= sup ((F # x) ^\ 0) by NAT_1:47; then A27: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27; (superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23; then P . x >= lim_sup (F # x) by A27, XXREAL_0:2; then P . x >= (lim_sup F) . x by A24, MESFUNC8:def_8; hence |.((lim_sup F) . x).| <= P . x by A26, EXTREAL2:12; ::_thesis: verum end; then lim_sup F is_integrable_on M by A2, A4, A23, A12, MESFUNC5:102; hence |.(lim_sup F).| is_integrable_on M by A23, A12, MESFUNC5:100; ::_thesis: verum end; Lm1: for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let M be sigma_Measure of S; ::_thesis: for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) & eq_dom (P,+infty) = {} implies ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) ) assume that A1: E = dom (F . 0) and A2: E = dom P and A3: for n being Nat holds F . n is_measurable_on E and A4: P is_integrable_on M and A5: P is nonnegative and A6: for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x and A7: eq_dom (P,+infty) = {} ; ::_thesis: ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) A8: E = dom (lim_inf F) by A1, MESFUNC8:def_7; then A9: (lim_inf F) | E = lim_inf F by RELAT_1:68; deffunc H1( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P + (F . \$1); consider G being Function such that A10: ( dom G = NAT & ( for n being Element of NAT holds G . n = H1(n) ) ) from FUNCT_1:sch_4(); A11: for x being Element of X for k being Nat st x in E holds ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) proof let x be Element of X; ::_thesis: for k being Nat st x in E holds ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) let k be Nat; ::_thesis: ( x in E implies ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) ) assume A12: x in E ; ::_thesis: ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) then x in dom (F . k) by A1, MESFUNC8:def_2; then A13: x in dom |.(F . k).| by MESFUNC1:def_10; |.(F . k).| . x <= P . x by A6, A12; then A14: |.((F . k) . x).| <= P . x by A13, MESFUNC1:def_10; then A15: (F . k) . x <= P . x by EXTREAL2:12; - (P . x) <= (F . k) . x by A14, EXTREAL2:12; hence ( - (P . x) <= (F # x) . k & (F # x) . k <= P . x ) by A15, MESFUNC5:def_13; ::_thesis: verum end; A16: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F)_holds_ |.((lim_inf_F)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (lim_inf F) implies |.((lim_inf F) . x).| <= P . x ) assume A17: x in dom (lim_inf F) ; ::_thesis: |.((lim_inf F) . x).| <= P . x now__::_thesis:_for_k_being_Nat_holds_(inferior_realsequence_(F_#_x))_._k_<=_P_._x let k be Nat; ::_thesis: (inferior_realsequence (F # x)) . k <= P . x k is Element of NAT by ORDINAL1:def_12; then A18: (inferior_realsequence (F # x)) . k <= (F # x) . k by RINFSUP2:8; (F # x) . k <= P . x by A8, A11, A17; hence (inferior_realsequence (F # x)) . k <= P . x by A18, XXREAL_0:2; ::_thesis: verum end; then lim_inf (F # x) <= P . x by Th5; then A19: (lim_inf F) . x <= P . x by A17, MESFUNC8:def_7; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_ -_(P_._x)_<=_y let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies - (P . x) <= y ) assume y in rng (F # x) ; ::_thesis: - (P . x) <= y then ex k being set st ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3; hence - (P . x) <= y by A8, A11, A17; ::_thesis: verum end; then - (P . x) is LowerBound of rng (F # x) by XXREAL_2:def_2; then - (P . x) <= inf (rng (F # x)) by XXREAL_2:def_4; then - (P . x) <= inf ((F # x) ^\ 0) by NAT_1:47; then A20: - (P . x) <= (inferior_realsequence (F # x)) . 0 by RINFSUP2:27; (inferior_realsequence (F # x)) . 0 <= sup (inferior_realsequence (F # x)) by RINFSUP2:23; then - (P . x) <= lim_inf (F # x) by A20, XXREAL_0:2; then - (P . x) <= (lim_inf F) . x by A17, MESFUNC8:def_7; hence |.((lim_inf F) . x).| <= P . x by A19, EXTREAL2:12; ::_thesis: verum end; lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24; then lim_inf F is_integrable_on M by A2, A4, A8, A16, MESFUNC5:102; then A21: ex E3 being Element of S st ( E3 = (dom P) /\ (dom (lim_inf F)) & Integral (M,(P + (lim_inf F))) = (Integral (M,(P | E3))) + (Integral (M,((lim_inf F) | E3))) ) by A4, MESFUNC5:109; A22: P | E = P by A2, RELAT_1:68; A23: Integral (M,P) < +infty by A4, MESFUNC5:96; -infty < Integral (M,P) by A4, MESFUNC5:96; then A24: Integral (M,P) is Real by A23, XXREAL_0:14; now__::_thesis:_for_x_being_set_holds_not_x_in_P_"_{-infty} let x be set ; ::_thesis: not x in P " {-infty} assume x in P " {-infty} ; ::_thesis: contradiction then A25: P . x in {-infty} by FUNCT_1:def_7; 0 <= P . x by A5, SUPINF_2:51; hence contradiction by A25, TARSKI:def_1; ::_thesis: verum end; then A26: P " {-infty} = {} by XBOOLE_0:def_1; A27: now__::_thesis:_for_n_being_Element_of_NAT_holds_G_._n_is_PartFunc_of_X,ExtREAL let n be Element of NAT ; ::_thesis: G . n is PartFunc of X,ExtREAL G . n = P + (F . n) by A10; hence G . n is PartFunc of X,ExtREAL ; ::_thesis: verum end; A28: now__::_thesis:_for_n_being_Nat_holds_G_._n_=_P_+_(F_._n) let n be Nat; ::_thesis: G . n = P + (F . n) n is Element of NAT by ORDINAL1:def_12; hence G . n = P + (F . n) by A10; ::_thesis: verum end; reconsider G = G as Functional_Sequence of X,ExtREAL by A10, A27, SEQFUNC:1; A29: P " {+infty} = {} by A7, MESFUNC5:30; A30: for n being Nat holds dom (G . n) = E proof let n be Nat; ::_thesis: dom (G . n) = E dom (G . n) = dom (P + (F . n)) by A28; then A31: dom (G . n) = ((dom P) /\ (dom (F . n))) \ (((P " {-infty}) /\ ((F . n) " {+infty})) \/ ((P " {+infty}) /\ ((F . n) " {-infty}))) by MESFUNC1:def_3; dom (F . n) = E by A1, MESFUNC8:def_2; hence dom (G . n) = E by A2, A29, A26, A31; ::_thesis: verum end; A32: now__::_thesis:_for_n,_m_being_Nat_holds_dom_(G_._n)_=_dom_(G_._m) let n, m be Nat; ::_thesis: dom (G . n) = dom (G . m) thus dom (G . n) = E by A30 .= dom (G . m) by A30 ; ::_thesis: verum end; deffunc H2( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = P - (F . \$1); consider H being Function such that A33: ( dom H = NAT & ( for n being Element of NAT holds H . n = H2(n) ) ) from FUNCT_1:sch_4(); reconsider G = G as with_the_same_dom Functional_Sequence of X,ExtREAL by A32, MESFUNC8:def_2; A34: dom (G . 0) = dom (F . 0) by A1, A30; A35: for n being Nat holds F . n is_integrable_on M proof let n be Nat; ::_thesis: F . n is_integrable_on M A36: E = dom (F . n) by A1, MESFUNC8:def_2; A37: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_ |.((F_._n)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (F . n) implies |.((F . n) . x).| <= P . x ) assume A38: x in dom (F . n) ; ::_thesis: |.((F . n) . x).| <= P . x then A39: x in dom |.(F . n).| by MESFUNC1:def_10; |.(F . n).| . x <= P . x by A6, A36, A38; hence |.((F . n) . x).| <= P . x by A39, MESFUNC1:def_10; ::_thesis: verum end; F . n is_measurable_on E by A3; hence F . n is_integrable_on M by A2, A4, A36, A37, MESFUNC5:102; ::_thesis: verum end; A40: now__::_thesis:_for_n_being_Nat_holds_ (_G_._n_is_nonnegative_&_G_._n_is_measurable_on_E_) let n be Nat; ::_thesis: ( G . n is nonnegative & G . n is_measurable_on E ) A41: G . n = P + (F . n) by A28; now__::_thesis:_for_x_being_set_st_x_in_dom_(P_+_(F_._n))_holds_ 0_<=_(P_+_(F_._n))_._x let x be set ; ::_thesis: ( x in dom (P + (F . n)) implies 0 <= (P + (F . n)) . x ) assume A42: x in dom (P + (F . n)) ; ::_thesis: 0 <= (P + (F . n)) . x then reconsider x1 = x as Element of X ; x in E by A30, A41, A42; then - (P . x) <= (F # x1) . n by A11; then A43: - (P . x) <= (F . n) . x by MESFUNC5:def_13; (- (P . x)) + (P . x) = 0 by XXREAL_3:7; then 0 <= ((F . n) . x) + (P . x) by A43, XXREAL_3:36; hence 0 <= (P + (F . n)) . x by A42, MESFUNC1:def_3; ::_thesis: verum end; hence G . n is nonnegative by A41, SUPINF_2:52; ::_thesis: G . n is_measurable_on E F . n is_integrable_on M by A35; then G . n is_integrable_on M by A4, A41, MESFUNC5:108; then ex E1 being Element of S st ( E1 = dom (G . n) & G . n is_measurable_on E1 ) by MESFUNC5:def_17; hence G . n is_measurable_on E by A30; ::_thesis: verum end; E = dom (G . 0) by A30; then consider IG being ExtREAL_sequence such that A44: for n being Nat holds IG . n = Integral (M,(G . n)) and A45: Integral (M,(lim_inf G)) <= lim_inf IG by A40, Th7; A46: Integral (M,P) < +infty by A4, MESFUNC5:96; deffunc H3( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . \$1)); consider I being Function of NAT,ExtREAL such that A47: for n being Element of NAT holds I . n = H3(n) from FUNCT_2:sch_4(); reconsider I = I as ExtREAL_sequence ; A48: -infty < Integral (M,P) by A4, MESFUNC5:96; A49: for n being Nat holds ( I . n = Integral (M,(F . n)) & I . n is Real ) proof let n be Nat; ::_thesis: ( I . n = Integral (M,(F . n)) & I . n is Real ) n is Element of NAT by ORDINAL1:def_12; then A50: I . n = Integral (M,(F . n)) by A47; A51: F . n is_integrable_on M by A35; then A52: Integral (M,(F . n)) < +infty by MESFUNC5:96; -infty < Integral (M,(F . n)) by A51, MESFUNC5:96; hence ( I . n = Integral (M,(F . n)) & I . n is Real ) by A50, A52, XXREAL_0:14; ::_thesis: verum end; now__::_thesis:_for_n_being_Nat_holds_IG_._n_=_(Integral_(M,P))_+_(I_._n) let n be Nat; ::_thesis: IG . n = (Integral (M,P)) + (I . n) A53: G . n = P + (F . n) by A28; F . n is_integrable_on M by A35; then A54: ex E2 being Element of S st ( E2 = (dom P) /\ (dom (F . n)) & Integral (M,(G . n)) = (Integral (M,(P | E2))) + (Integral (M,((F . n) | E2))) ) by A4, A53, MESFUNC5:109; A55: P | E = P by A2, RELAT_1:68; A56: dom (F . n) = E by A1, MESFUNC8:def_2; then (F . n) | E = F . n by RELAT_1:68; then Integral (M,(G . n)) = (Integral (M,P)) + (I . n) by A2, A49, A54, A56, A55; hence IG . n = (Integral (M,P)) + (I . n) by A44; ::_thesis: verum end; then lim_inf IG = (Integral (M,P)) + (lim_inf I) by A24, Th10; then (Integral (M,P)) + (Integral (M,(lim_inf F))) <= (Integral (M,P)) + (lim_inf I) by A2, A8, A28, A29, A26, A45, A21, A22, A9, A34, Th11; then Integral (M,(lim_inf F)) <= ((lim_inf I) + (Integral (M,P))) - (Integral (M,P)) by A48, A46, XXREAL_3:56; then Integral (M,(lim_inf F)) <= (lim_inf I) + ((Integral (M,P)) - (Integral (M,P))) by A48, A46, XXREAL_3:30; then Integral (M,(lim_inf F)) <= (lim_inf I) + 0. by XXREAL_3:7; then A57: Integral (M,(lim_inf F)) <= lim_inf I by XXREAL_3:4; A58: now__::_thesis:_for_n_being_Element_of_NAT_holds_H_._n_is_PartFunc_of_X,ExtREAL let n be Element of NAT ; ::_thesis: H . n is PartFunc of X,ExtREAL H . n = P - (F . n) by A33; hence H . n is PartFunc of X,ExtREAL ; ::_thesis: verum end; A59: now__::_thesis:_for_n_being_Nat_holds_H_._n_=_P_-_(F_._n) let n be Nat; ::_thesis: H . n = P - (F . n) n is Element of NAT by ORDINAL1:def_12; hence H . n = P - (F . n) by A33; ::_thesis: verum end; A60: E = dom (lim_sup F) by A1, MESFUNC8:def_8; A61: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F)_holds_ |.((lim_sup_F)_._x).|_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (lim_sup F) implies |.((lim_sup F) . x).| <= P . x ) assume A62: x in dom (lim_sup F) ; ::_thesis: |.((lim_sup F) . x).| <= P . x for k being Nat holds (superior_realsequence (F # x)) . k >= - (P . x) proof let k be Nat; ::_thesis: (superior_realsequence (F # x)) . k >= - (P . x) k is Element of NAT by ORDINAL1:def_12; then A63: (superior_realsequence (F # x)) . k >= (F # x) . k by RINFSUP2:8; (F # x) . k >= - (P . x) by A60, A11, A62; hence (superior_realsequence (F # x)) . k >= - (P . x) by A63, XXREAL_0:2; ::_thesis: verum end; then lim_sup (F # x) >= - (P . x) by Th4; then A64: (lim_sup F) . x >= - (P . x) by A62, MESFUNC8:def_8; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(F_#_x)_holds_ P_._x_>=_y let y be ext-real number ; ::_thesis: ( y in rng (F # x) implies P . x >= y ) assume y in rng (F # x) ; ::_thesis: P . x >= y then ex k being set st ( k in dom (F # x) & y = (F # x) . k ) by FUNCT_1:def_3; hence P . x >= y by A60, A11, A62; ::_thesis: verum end; then P . x is UpperBound of rng (F # x) by XXREAL_2:def_1; then P . x >= sup (rng (F # x)) by XXREAL_2:def_3; then P . x >= sup ((F # x) ^\ 0) by NAT_1:47; then A65: P . x >= (superior_realsequence (F # x)) . 0 by RINFSUP2:27; (superior_realsequence (F # x)) . 0 >= inf (superior_realsequence (F # x)) by RINFSUP2:23; then P . x >= lim_sup (F # x) by A65, XXREAL_0:2; then P . x >= (lim_sup F) . x by A62, MESFUNC8:def_8; hence |.((lim_sup F) . x).| <= P . x by A64, EXTREAL2:12; ::_thesis: verum end; lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23; then A66: lim_sup F is_integrable_on M by A2, A4, A60, A61, MESFUNC5:102; then A67: ex E6 being Element of S st ( E6 = (dom P) /\ (dom (lim_sup F)) & Integral (M,(P - (lim_sup F))) = (Integral (M,(P | E6))) + (Integral (M,((- (lim_sup F)) | E6))) ) by A4, Th13; set E1 = Integral (M,(lim_sup F)); A68: Integral (M,(lim_sup F)) < +infty by A66, MESFUNC5:96; -infty < Integral (M,(lim_sup F)) by A66, MESFUNC5:96; then reconsider e1 = Integral (M,(lim_sup F)) as Real by A68, XXREAL_0:14; A69: - (Integral (M,(lim_sup F))) = - e1 by SUPINF_2:2; A70: P | E = P by A2, RELAT_1:68; deffunc H4( Element of NAT ) -> Element of K6(K7(X,ExtREAL)) = - (F . \$1); consider F1 being Function such that A71: ( dom F1 = NAT & ( for n being Element of NAT holds F1 . n = H4(n) ) ) from FUNCT_1:sch_4(); reconsider H = H as Functional_Sequence of X,ExtREAL by A33, A58, SEQFUNC:1; A72: now__::_thesis:_for_n_being_Nat_holds_dom_(H_._n)_=_E let n be Nat; ::_thesis: dom (H . n) = E A73: dom (H . n) = dom (P - (F . n)) by A59; dom (F . n) = E by A1, MESFUNC8:def_2; then dom (H . n) = (E /\ E) \ (({} /\ ((F . n) " {+infty})) \/ ({} /\ ((F . n) " {-infty}))) by A2, A29, A26, A73, MESFUNC1:def_4; hence dom (H . n) = E ; ::_thesis: verum end; now__::_thesis:_for_n,_m_being_Nat_holds_dom_(H_._n)_=_dom_(H_._m) let n, m be Nat; ::_thesis: dom (H . n) = dom (H . m) thus dom (H . n) = E by A72 .= dom (H . m) by A72 ; ::_thesis: verum end; then reconsider H = H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2; A74: -infty < Integral (M,P) by A4, MESFUNC5:96; A75: now__::_thesis:_for_n_being_Nat_holds_ (_H_._n_is_nonnegative_&_H_._n_is_measurable_on_E_) let n be Nat; ::_thesis: ( H . n is nonnegative & H . n is_measurable_on E ) A76: H . n = P - (F . n) by A59; now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(F_._n)_holds_ (F_._n)_._x_<=_P_._x let x be Element of X; ::_thesis: ( x in dom (F . n) implies (F . n) . x <= P . x ) assume x in dom (F . n) ; ::_thesis: (F . n) . x <= P . x then x in E by A1, MESFUNC8:def_2; then (F # x) . n <= P . x by A11; hence (F . n) . x <= P . x by MESFUNC5:def_13; ::_thesis: verum end; hence H . n is nonnegative by A76, MESFUNC7:1; ::_thesis: H . n is_measurable_on E F . n is_integrable_on M by A35; then H . n is_integrable_on M by A4, A76, Th12; then ex E4 being Element of S st ( E4 = dom (H . n) & H . n is_measurable_on E4 ) by MESFUNC5:def_17; hence H . n is_measurable_on E by A72; ::_thesis: verum end; E = dom (H . 0) by A72; then consider IH being ExtREAL_sequence such that A77: for n being Nat holds IH . n = Integral (M,(H . n)) and A78: Integral (M,(lim_inf H)) <= lim_inf IH by A75, Th7; A79: Integral (M,P) < +infty by A4, MESFUNC5:96; now__::_thesis:_for_n_being_Element_of_NAT_holds_F1_._n_is_PartFunc_of_X,ExtREAL let n be Element of NAT ; ::_thesis: F1 . n is PartFunc of X,ExtREAL F1 . n = - (F . n) by A71; hence F1 . n is PartFunc of X,ExtREAL ; ::_thesis: verum end; then reconsider F1 = F1 as Functional_Sequence of X,ExtREAL by A71, SEQFUNC:1; A80: now__::_thesis:_for_n_being_Nat_holds_F1_._n_=_-_(F_._n) let n be Nat; ::_thesis: F1 . n = - (F . n) n is Element of NAT by ORDINAL1:def_12; hence F1 . n = - (F . n) by A71; ::_thesis: verum end; now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F1_._n)_=_dom_(F1_._m) let n, m be Nat; ::_thesis: dom (F1 . n) = dom (F1 . m) F1 . m = - (F . m) by A80; then A81: dom (F1 . m) = dom (F . m) by MESFUNC1:def_7; F1 . n = - (F . n) by A80; then dom (F1 . n) = dom (F . n) by MESFUNC1:def_7; hence dom (F1 . n) = dom (F1 . m) by A81, MESFUNC8:def_2; ::_thesis: verum end; then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2; A82: Integral (M,(- (lim_sup F))) = Integral (M,((- 1) (#) (lim_sup F))) by MESFUNC2:9; A83: now__::_thesis:_for_n_being_Nat_holds_H_._n_=_P_+_(F1_._n) let n be Nat; ::_thesis: H . n = P + (F1 . n) H . n = P - (F . n) by A59; then H . n = P + (- (F . n)) by MESFUNC2:8; hence H . n = P + (F1 . n) by A80; ::_thesis: verum end; F1 . 0 = - (F . 0) by A80; then A84: dom (F1 . 0) = dom (F . 0) by MESFUNC1:def_7; then dom (F1 . 0) = dom (H . 0) by A1, A72; then lim_inf H = P + (lim_inf F1) by A29, A26, A83, Th11; then lim_inf H = P + (- (lim_sup F)) by A80, A84, Th15; then A85: lim_inf H = P - (lim_sup F) by MESFUNC2:8; E = dom (lim_sup F) by A1, MESFUNC8:def_8; then E = dom (- (lim_sup F)) by MESFUNC1:def_7; then A86: (- (lim_sup F)) | E = - (lim_sup F) by RELAT_1:68; deffunc H5( Element of NAT ) -> Element of ExtREAL = - (I . \$1); consider I1 being Function of NAT,ExtREAL such that A87: for n being Element of NAT holds I1 . n = H5(n) from FUNCT_2:sch_4(); reconsider I1 = I1 as ExtREAL_sequence ; A88: now__::_thesis:_for_n_being_Nat_holds_I1_._n_=_-_(I_._n) let n be Nat; ::_thesis: I1 . n = - (I . n) n is Element of NAT by ORDINAL1:def_12; hence I1 . n = - (I . n) by A87; ::_thesis: verum end; then A89: - (lim_inf I1) = lim_sup I by Th14; now__::_thesis:_for_n_being_Nat_holds_IH_._n_=_(Integral_(M,P))_+_(I1_._n) let n be Nat; ::_thesis: IH . n = (Integral (M,P)) + (I1 . n) A90: F . n is_integrable_on M by A35; Integral (M,(- (F . n))) = Integral (M,((- 1) (#) (F . n))) by MESFUNC2:9; then A91: Integral (M,(- (F . n))) = (R_EAL (- 1)) * (Integral (M,(F . n))) by A90, MESFUNC5:110; A92: dom (F . n) = E by A1, MESFUNC8:def_2; then E = dom (- (F . n)) by MESFUNC1:def_7; then A93: (- (F . n)) | E = - (F . n) by RELAT_1:68; H . n = P - (F . n) by A59; then A94: ex E5 being Element of S st ( E5 = (dom P) /\ (dom (F . n)) & Integral (M,(H . n)) = (Integral (M,(P | E5))) + (Integral (M,((- (F . n)) | E5))) ) by A4, A90, Th13; reconsider In = I . n as Real by A49; A95: (R_EAL (- 1)) * (I . n) = (- 1) * In by EXTREAL1:1; A96: - (I . n) = - In by SUPINF_2:2; P | E = P by A2, RELAT_1:68; then Integral (M,(H . n)) = (Integral (M,P)) + (- (I . n)) by A2, A49, A94, A92, A93, A91, A95, A96; then IH . n = (Integral (M,P)) + (- (I . n)) by A77; hence IH . n = (Integral (M,P)) + (I1 . n) by A88; ::_thesis: verum end; then lim_inf IH = (Integral (M,P)) + (lim_inf I1) by A24, Th10; then (Integral (M,P)) + ((R_EAL (- 1)) * (Integral (M,(lim_sup F)))) <= (Integral (M,P)) + (- (lim_sup I)) by A2, A60, A78, A89, A85, A66, A67, A70, A86, A82, MESFUNC5:110; then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= ((- (lim_sup I)) + (Integral (M,P))) - (Integral (M,P)) by A74, A79, XXREAL_3:56; then (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + ((Integral (M,P)) - (Integral (M,P))) by A74, A79, XXREAL_3:30; then A97: (R_EAL (- 1)) * (Integral (M,(lim_sup F))) <= (- (lim_sup I)) + 0. by XXREAL_3:7; (R_EAL (- 1)) * (Integral (M,(lim_sup F))) = (- 1) * e1 by EXTREAL1:1; then - (Integral (M,(lim_sup F))) <= - (lim_sup I) by A97, A69, XXREAL_3:4; then A98: Integral (M,(lim_sup F)) >= lim_sup I by XXREAL_3:38; now__::_thesis:_(_(_for_x_being_Element_of_X_st_x_in_E_holds_ F_#_x_is_convergent_)_implies_(_I_is_convergent_&_lim_I_=_Integral_(M,(lim_F))_)_) A99: lim_inf I <= lim_sup I by RINFSUP2:39; A100: dom (lim F) = dom (F . 0) by MESFUNC8:def_9; assume A101: for x being Element of X st x in E holds F # x is convergent ; ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) ) A102: for x being Element of X st x in dom (lim F) holds (lim F) . x = (lim_inf F) . x proof let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x ) assume A103: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x then F # x is convergent by A1, A101, A100; hence (lim F) . x = (lim_inf F) . x by A103, MESFUNC8:14; ::_thesis: verum end; A104: for x being Element of X st x in dom (lim F) holds (lim F) . x = (lim_sup F) . x proof let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x ) assume A105: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_sup F) . x then F # x is convergent by A1, A101, A100; hence (lim F) . x = (lim_sup F) . x by A105, MESFUNC8:14; ::_thesis: verum end; A106: dom (lim F) = dom (lim_sup F) by A100, MESFUNC8:def_8; then A107: lim F = lim_sup F by A104, PARTFUN1:5; A108: dom (lim F) = dom (lim_inf F) by A100, MESFUNC8:def_7; then Integral (M,(lim F)) <= lim_inf I by A57, A102, PARTFUN1:5; then lim_sup I <= lim_inf I by A98, A107, XXREAL_0:2; then lim_inf I = lim_sup I by A99, XXREAL_0:1; hence A109: I is convergent by RINFSUP2:40; ::_thesis: lim I = Integral (M,(lim F)) then lim I = lim_sup I by RINFSUP2:41; then A110: lim I <= Integral (M,(lim F)) by A98, A106, A104, PARTFUN1:5; lim I = lim_inf I by A109, RINFSUP2:41; then Integral (M,(lim F)) <= lim I by A57, A108, A102, PARTFUN1:5; hence lim I = Integral (M,(lim F)) by A110, XXREAL_0:1; ::_thesis: verum end; hence ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A49, A57, A98; ::_thesis: verum end; theorem Th17: :: MESFUN10:17 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let M be sigma_Measure of S; ::_thesis: for E being Element of S for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let E be Element of S; ::_thesis: for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) let P be PartFunc of X,ExtREAL; ::_thesis: ( E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is_measurable_on E ) & P is_integrable_on M & P is nonnegative & ( for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ) implies ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) ) assume that A1: E = dom (F . 0) and A2: E = dom P and A3: for n being Nat holds F . n is_measurable_on E and A4: P is_integrable_on M and A5: P is nonnegative and A6: for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= P . x ; ::_thesis: ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) for x being set st x in eq_dom (P,+infty) holds x in E by A2, MESFUNC1:def_15; then eq_dom (P,+infty) c= E by TARSKI:def_3; then A7: eq_dom (P,+infty) = E /\ (eq_dom (P,+infty)) by XBOOLE_1:28; ex A being Element of S st ( A = dom P & P is_measurable_on A ) by A4, MESFUNC5:def_17; then reconsider E0 = eq_dom (P,+infty) as Element of S by A2, A7, MESFUNC1:33; reconsider E1 = E \ E0 as Element of S ; deffunc H1( Nat) -> Element of K6(K7(X,ExtREAL)) = (F . \$1) | E1; consider F1 being Functional_Sequence of X,ExtREAL such that A8: for n being Nat holds F1 . n = H1(n) from SEQFUNC:sch_1(); A9: now__::_thesis:_for_n_being_Nat_holds_dom_(F1_._n)_=_E1 let n be Nat; ::_thesis: dom (F1 . n) = E1 dom (F . n) = E by A1, MESFUNC8:def_2; then dom ((F . n) | E1) = E1 by RELAT_1:62, XBOOLE_1:36; hence dom (F1 . n) = E1 by A8; ::_thesis: verum end; then A10: E1 = dom (F1 . 0) ; now__::_thesis:_for_n,_m_being_Nat_holds_dom_(F1_._n)_=_dom_(F1_._m) let n, m be Nat; ::_thesis: dom (F1 . n) = dom (F1 . m) thus dom (F1 . n) = E1 by A9 .= dom (F1 . m) by A9 ; ::_thesis: verum end; then reconsider F1 = F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def_2; set P1 = P | E1; A11: P | E1 is nonnegative by A5, MESFUNC5:15; A12: E1 c= E by XBOOLE_1:36; A13: now__::_thesis:_for_x_being_Element_of_X for_n_being_Nat_st_x_in_E1_holds_ |.(F1_._n).|_._x_<=_(P_|_E1)_._x let x be Element of X; ::_thesis: for n being Nat st x in E1 holds |.(F1 . n).| . x <= (P | E1) . x let n be Nat; ::_thesis: ( x in E1 implies |.(F1 . n).| . x <= (P | E1) . x ) assume A14: x in E1 ; ::_thesis: |.(F1 . n).| . x <= (P | E1) . x then A15: (P | E1) . x = P . x by FUNCT_1:49; x in E by A12, A14; then x in dom (F . n) by A1, MESFUNC8:def_2; then x in dom |.(F . n).| by MESFUNC1:def_10; then A16: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def_10; E1 = dom (F1 . n) by A9; then A17: E1 = dom |.(F1 . n).| by MESFUNC1:def_10; F1 . n = (F . n) | E1 by A8; then (F1 . n) . x = (F . n) . x by A14, FUNCT_1:49; then |.(F . n).| . x = |.(F1 . n).| . x by A14, A16, A17, MESFUNC1:def_10; hence |.(F1 . n).| . x <= (P | E1) . x by A6, A12, A14, A15; ::_thesis: verum end; A18: dom (lim F) = dom (F . 0) by MESFUNC8:def_9; then A19: dom (lim F) = dom (lim_inf F) by MESFUNC8:def_7; A20: dom (lim_inf F) = E by A1, MESFUNC8:def_7; A21: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_inf_F1)_holds_ ((lim_inf_F)_|_(E_\_E0))_._x_=_(lim_inf_F1)_._x let x be Element of X; ::_thesis: ( x in dom (lim_inf F1) implies ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x ) assume A22: x in dom (lim_inf F1) ; ::_thesis: ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x then A23: x in E1 by A10, MESFUNC8:def_7; now__::_thesis:_for_n_being_Element_of_NAT_holds_(F1_#_x)_._n_=_(F_#_x)_._n let n be Element of NAT ; ::_thesis: (F1 # x) . n = (F # x) . n ((F . n) | E1) . x = (F . n) . x by A23, FUNCT_1:49; then (F1 . n) . x = (F . n) . x by A8; then (F1 # x) . n = (F . n) . x by MESFUNC5:def_13; hence (F1 # x) . n = (F # x) . n by MESFUNC5:def_13; ::_thesis: verum end; then A24: F1 # x = F # x by FUNCT_2:63; E1 = dom (lim_inf F1) by A10, MESFUNC8:def_7; then lim_inf (F # x) = (lim_inf F) . x by A12, A20, A22, MESFUNC8:def_7; then (lim_inf F1) . x = (lim_inf F) . x by A22, A24, MESFUNC8:def_7; hence ((lim_inf F) | (E \ E0)) . x = (lim_inf F1) . x by A23, FUNCT_1:49; ::_thesis: verum end; E1 = dom ((lim_inf F) | (E \ E0)) by A20, RELAT_1:62, XBOOLE_1:36; then dom ((lim_inf F) | (E \ E0)) = dom (lim_inf F1) by A10, MESFUNC8:def_7; then A25: (lim_inf F) | (E \ E0) = lim_inf F1 by A21, PARTFUN1:5; A26: dom (lim_sup F) = E by A1, MESFUNC8:def_8; A27: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_sup_F1)_holds_ ((lim_sup_F)_|_(E_\_E0))_._x_=_(lim_sup_F1)_._x let x be Element of X; ::_thesis: ( x in dom (lim_sup F1) implies ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x ) assume A28: x in dom (lim_sup F1) ; ::_thesis: ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x then A29: x in E1 by A10, MESFUNC8:def_8; now__::_thesis:_for_n_being_Element_of_NAT_holds_(F1_#_x)_._n_=_(F_#_x)_._n let n be Element of NAT ; ::_thesis: (F1 # x) . n = (F # x) . n ((F . n) | E1) . x = (F . n) . x by A29, FUNCT_1:49; then (F1 . n) . x = (F . n) . x by A8; then (F1 # x) . n = (F . n) . x by MESFUNC5:def_13; hence (F1 # x) . n = (F # x) . n by MESFUNC5:def_13; ::_thesis: verum end; then A30: F1 # x = F # x by FUNCT_2:63; E1 = dom (lim_sup F1) by A10, MESFUNC8:def_8; then lim_sup (F # x) = (lim_sup F) . x by A12, A26, A28, MESFUNC8:def_8; then (lim_sup F1) . x = (lim_sup F) . x by A28, A30, MESFUNC8:def_8; hence ((lim_sup F) | (E \ E0)) . x = (lim_sup F1) . x by A29, FUNCT_1:49; ::_thesis: verum end; E1 = dom ((lim_sup F) | (E \ E0)) by A26, RELAT_1:62, XBOOLE_1:36; then dom ((lim_sup F) | (E \ E0)) = dom (lim_sup F1) by A10, MESFUNC8:def_8; then A31: (lim_sup F) | (E \ E0) = lim_sup F1 by A27, PARTFUN1:5; A32: dom (P | E1) = E1 by A2, RELAT_1:62, XBOOLE_1:36; A33: now__::_thesis:_not_eq_dom_((P_|_E1),+infty)_<>_{} assume eq_dom ((P | E1),+infty) <> {} ; ::_thesis: contradiction then consider x being set such that A34: x in eq_dom ((P | E1),+infty) by XBOOLE_0:def_1; reconsider x = x as Element of X by A34; (P | E1) . x = +infty by A34, MESFUNC1:def_15; then consider y being R_eal such that A35: y = (P | E1) . x and A36: +infty = y ; A37: x in E1 by A32, A34, MESFUNC1:def_15; then y = P . x by A35, FUNCT_1:49; then x in eq_dom (P,+infty) by A2, A12, A36, A37, MESFUNC1:def_15; hence contradiction by A37, XBOOLE_0:def_5; ::_thesis: verum end; A38: for n being Nat holds F1 . n is_measurable_on E1 proof let n be Nat; ::_thesis: F1 . n is_measurable_on E1 dom (F . n) = E by A1, MESFUNC8:def_2; then A39: E1 = (dom (F . n)) /\ E1 by XBOOLE_1:28, XBOOLE_1:36; F . n is_measurable_on E by A3; then F . n is_measurable_on E1 by MESFUNC1:30, XBOOLE_1:36; then (F . n) | E1 is_measurable_on E1 by A39, MESFUNC5:42; hence F1 . n is_measurable_on E1 by A8; ::_thesis: verum end; P | E1 is_integrable_on M by A4, MESFUNC5:112; then consider I being ExtREAL_sequence such that A40: for n being Nat holds I . n = Integral (M,(F1 . n)) and A41: lim_inf I >= Integral (M,(lim_inf F1)) and A42: lim_sup I <= Integral (M,(lim_sup F1)) and ( ( for x being Element of X st x in E1 holds F1 # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F1)) ) ) by A32, A10, A11, A13, A38, A33, Lm1; P " {+infty} = E0 by MESFUNC5:30; then A43: M . E0 = 0 by A4, MESFUNC5:105; A44: for n being Nat holds I . n = Integral (M,(F . n)) proof let n be Nat; ::_thesis: I . n = Integral (M,(F . n)) A45: E = dom (F . n) by A1, MESFUNC8:def_2; A46: F . n is_measurable_on E by A3; |.(F . n).| is_integrable_on M by A1, A2, A3, A4, A6, Th16; then F . n is_integrable_on M by A45, A46, MESFUNC5:100; then Integral (M,(F . n)) = (Integral (M,((F . n) | E0))) + (Integral (M,((F . n) | E1))) by A45, MESFUNC5:99; then A47: Integral (M,(F . n)) = 0. + (Integral (M,((F . n) | E1))) by A3, A43, A45, MESFUNC5:94; I . n = Integral (M,(F1 . n)) by A40; then I . n = Integral (M,((F . n) | E1)) by A8; hence I . n = Integral (M,(F . n)) by A47, XXREAL_3:4; ::_thesis: verum end; lim_inf F is_measurable_on E by A1, A3, MESFUNC8:24; then A48: Integral (M,((lim_inf F) | (E \ E0))) = Integral (M,(lim_inf F)) by A43, A20, MESFUNC5:95; lim_sup F is_measurable_on E by A1, A3, MESFUNC8:23; then A49: Integral (M,((lim_sup F) | (E \ E0))) = Integral (M,(lim_sup F)) by A43, A26, MESFUNC5:95; A50: dom (lim F) = dom (lim_sup F) by A18, MESFUNC8:def_8; now__::_thesis:_(_(_for_x_being_Element_of_X_st_x_in_E_holds_ F_#_x_is_convergent_)_implies_(_I_is_convergent_&_lim_I_=_Integral_(M,(lim_F))_)_) assume A51: for x being Element of X st x in E holds F # x is convergent ; ::_thesis: ( I is convergent & lim I = Integral (M,(lim F)) ) A52: for x being Element of X st x in dom (lim F) holds (lim F) . x = (lim_inf F) . x proof let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x ) assume A53: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x then F # x is convergent by A1, A18, A51; hence (lim F) . x = (lim_inf F) . x by A53, MESFUNC8:14; ::_thesis: verum end; then A54: lim F = lim_inf F by A19, PARTFUN1:5; A55: lim_inf I <= lim_sup I by RINFSUP2:39; A56: for x being Element of X st x in dom (lim F) holds (lim F) . x = (lim_sup F) . x proof let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_sup F) . x ) assume A57: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_sup F) . x then F # x is convergent by A1, A18, A51; hence (lim F) . x = (lim_sup F) . x by A57, MESFUNC8:14; ::_thesis: verum end; then lim F = lim_sup F by A50, PARTFUN1:5; then lim_sup I <= lim_inf I by A41, A42, A25, A31, A54, XXREAL_0:2; then lim_inf I = lim_sup I by A55, XXREAL_0:1; hence A58: I is convergent by RINFSUP2:40; ::_thesis: lim I = Integral (M,(lim F)) then lim I = lim_sup I by RINFSUP2:41; then A59: lim I <= Integral (M,(lim F)) by A42, A49, A31, A50, A56, PARTFUN1:5; lim I = lim_inf I by A58, RINFSUP2:41; then Integral (M,(lim F)) <= lim I by A41, A48, A25, A19, A52, PARTFUN1:5; hence lim I = Integral (M,(lim F)) by A59, XXREAL_0:1; ::_thesis: verum end; hence ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A41, A42, A44, A48, A49, A25, A31; ::_thesis: verum end; theorem :: MESFUN10:18 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) let M be sigma_Measure of S; ::_thesis: for E being Element of S st E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty holds ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) let E be Element of S; ::_thesis: ( E = dom (F . 0) & ( for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) ) & ( for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x ) & Integral (M,((F . 0) | E)) < +infty implies ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) assume that A1: E = dom (F . 0) and A2: for n being Nat holds ( F . n is nonnegative & F . n is_measurable_on E ) and A3: for x being Element of X for n, m being Nat st x in E & n <= m holds (F . n) . x >= (F . m) . x and A4: Integral (M,((F . 0) | E)) < +infty ; ::_thesis: ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) A5: F . 0 is nonnegative by A2; A6: dom (F . 0) = dom |.(F . 0).| by MESFUNC1:def_10; A7: for x being Element of X st x in dom (F . 0) holds (F . 0) . x = |.(F . 0).| . x proof let x be Element of X; ::_thesis: ( x in dom (F . 0) implies (F . 0) . x = |.(F . 0).| . x ) 0 <= (F . 0) . x by A5, SUPINF_2:51; then A8: |.((F . 0) . x).| = (F . 0) . x by EXTREAL1:def_1; assume x in dom (F . 0) ; ::_thesis: (F . 0) . x = |.(F . 0).| . x hence (F . 0) . x = |.(F . 0).| . x by A6, A8, MESFUNC1:def_10; ::_thesis: verum end; A9: F . 0 is_measurable_on E by A2; then Integral (M,(F . 0)) = integral+ (M,(F . 0)) by A1, A5, MESFUNC5:88; then integral+ (M,(F . 0)) < +infty by A1, A4, RELAT_1:68; then A10: integral+ (M,|.(F . 0).|) < +infty by A6, A7, PARTFUN1:5; A11: max+ (F . 0) is_measurable_on E by A2, MESFUNC2:25; for x being set st x in dom (max- (F . 0)) holds 0. <= (max- (F . 0)) . x by MESFUNC2:13; then A12: max- (F . 0) is nonnegative by SUPINF_2:52; A13: for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= (F . 0) . x proof let x be Element of X; ::_thesis: for n being Nat st x in E holds |.(F . n).| . x <= (F . 0) . x let n be Nat; ::_thesis: ( x in E implies |.(F . n).| . x <= (F . 0) . x ) assume A14: x in E ; ::_thesis: |.(F . n).| . x <= (F . 0) . x F . n is nonnegative by A2; then 0 <= (F . n) . x by SUPINF_2:51; then |.((F . n) . x).| = (F . n) . x by EXTREAL1:def_1; then A15: |.((F . n) . x).| <= (F . 0) . x by A3, A14; dom (F . n) = dom |.(F . n).| by MESFUNC1:def_10; then x in dom |.(F . n).| by A1, A14, MESFUNC8:def_2; hence |.(F . n).| . x <= (F . 0) . x by A15, MESFUNC1:def_10; ::_thesis: verum end; A16: for x being Element of X st x in E holds F # x is convergent proof let x be Element of X; ::_thesis: ( x in E implies F # x is convergent ) assume A17: x in E ; ::_thesis: F # x is convergent now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (F_#_x)_._n_<=_(F_#_x)_._m let n, m be Element of NAT ; ::_thesis: ( m <= n implies (F # x) . n <= (F # x) . m ) assume m <= n ; ::_thesis: (F # x) . n <= (F # x) . m then (F . n) . x <= (F . m) . x by A3, A17; then (F # x) . n <= (F . m) . x by MESFUNC5:def_13; hence (F # x) . n <= (F # x) . m by MESFUNC5:def_13; ::_thesis: verum end; then F # x is non-increasing by RINFSUP2:7; hence F # x is convergent by RINFSUP2:36; ::_thesis: verum end; A18: dom (max+ (F . 0)) = dom (F . 0) by MESFUNC2:def_2; then A19: (max+ (F . 0)) | E = max+ (F . 0) by A1, RELAT_1:68; for x being set st x in dom (max+ (F . 0)) holds 0. <= (max+ (F . 0)) . x by MESFUNC2:12; then A20: max+ (F . 0) is nonnegative by SUPINF_2:52; then A21: dom ((max+ (F . 0)) + (max- (F . 0))) = (dom (max+ (F . 0))) /\ (dom (max- (F . 0))) by A12, MESFUNC5:22; A22: dom (max- (F . 0)) = dom (F . 0) by MESFUNC2:def_3; then A23: (max- (F . 0)) | E = max- (F . 0) by A1, RELAT_1:68; max- (F . 0) is_measurable_on E by A1, A2, MESFUNC2:26; then ex C being Element of S st ( C = dom ((max+ (F . 0)) + (max- (F . 0))) & integral+ (M,((max+ (F . 0)) + (max- (F . 0)))) = (integral+ (M,((max+ (F . 0)) | C))) + (integral+ (M,((max- (F . 0)) | C))) ) by A1, A18, A22, A20, A12, A11, MESFUNC5:78; then A24: (integral+ (M,(max+ (F . 0)))) + (integral+ (M,(max- (F . 0)))) < +infty by A1, A18, A22, A21, A19, A23, A10, MESFUNC2:24; 0 <= integral+ (M,(max- (F . 0))) by A1, A9, A22, A12, MESFUNC2:26, MESFUNC5:79; then integral+ (M,(max+ (F . 0))) <> +infty by A24, XXREAL_3:def_2; then A25: integral+ (M,(max+ (F . 0))) < +infty by XXREAL_0:4; 0 <= integral+ (M,(max+ (F . 0))) by A1, A9, A18, A20, MESFUNC2:25, MESFUNC5:79; then integral+ (M,(max- (F . 0))) <> +infty by A24, XXREAL_3:def_2; then integral+ (M,(max- (F . 0))) < +infty by XXREAL_0:4; then F . 0 is_integrable_on M by A1, A9, A25, MESFUNC5:def_17; then ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A1, A2, A13, Th17; hence ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) by A16; ::_thesis: verum end; definition let X be set ; let F be Functional_Sequence of X,ExtREAL; attrF is uniformly_bounded means :Def1: :: MESFUN10:def 1 ex K being real number st for n being Nat for x being set st x in dom (F . 0) holds |.((F . n) . x).| <= K; end; :: deftheorem Def1 defines uniformly_bounded MESFUN10:def_1_:_ for X being set for F being Functional_Sequence of X,ExtREAL holds ( F is uniformly_bounded iff ex K being real number st for n being Nat for x being set st x in dom (F . 0) holds |.((F . n) . x).| <= K ); theorem :: MESFUN10:19 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) holds ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) holds ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) holds ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) holds ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) let M be sigma_Measure of S; ::_thesis: for E being Element of S st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) holds ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) let E be Element of S; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_measurable_on E ) & F is uniformly_bounded & ( for x being Element of X st x in E holds F # x is convergent ) implies ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) ) assume that A1: M . E < +infty and A2: E = dom (F . 0) and A3: for n being Nat holds F . n is_measurable_on E and A4: F is uniformly_bounded and A5: for x being Element of X st x in E holds F # x is convergent ; ::_thesis: ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) consider K1 being real number such that A6: for n being Nat for x being set st x in dom (F . 0) holds |.((F . n) . x).| <= K1 by A4, Def1; set K = max (K1,1); max (K1,1) in REAL by XREAL_0:def_1; then consider h being PartFunc of X,ExtREAL such that A7: h is_simple_func_in S and A8: dom h = E and A9: for x being set st x in E holds h . x = max (K1,1) by MESFUNC5:41, NUMBERS:31; A10: dom h = dom |.h.| by MESFUNC1:def_10; A11: max (K1,1) > 0 by XXREAL_0:30; then A12: (R_EAL (max (K1,1))) * +infty = +infty by XXREAL_3:def_5; for x being set st x in E holds h . x >= 0. by A11, A9; then A13: h is nonnegative by A8, SUPINF_2:52; then A14: Integral (M,h) = integral' (M,h) by A7, MESFUNC5:89; max (K1,1) is Real by XREAL_0:def_1; then A15: integral' (M,h) = (R_EAL (max (K1,1))) * (M . (dom h)) by A11, A8, A9, MESFUNC5:104; A16: for x being Element of X st x in dom h holds h . x = |.h.| . x proof let x be Element of X; ::_thesis: ( x in dom h implies h . x = |.h.| . x ) assume x in dom h ; ::_thesis: h . x = |.h.| . x then A17: x in dom |.h.| by MESFUNC1:def_10; 0 <= h . x by A13, SUPINF_2:51; then |.(h . x).| = h . x by EXTREAL1:def_1; hence h . x = |.h.| . x by A17, MESFUNC1:def_10; ::_thesis: verum end; Integral (M,h) = integral+ (M,h) by A7, A13, MESFUNC5:89; then integral+ (M,h) < +infty by A1, A11, A8, A15, A12, A14, XXREAL_3:72; then A18: integral+ (M,|.h.|) < +infty by A10, A16, PARTFUN1:5; A19: dom (max+ h) = dom h by MESFUNC2:def_2; then A20: (max+ h) | E = max+ h by A8, RELAT_1:68; A21: max+ h is_measurable_on E by A7, MESFUNC2:25, MESFUNC2:34; for x being set st x in dom (max- h) holds 0. <= (max- h) . x by MESFUNC2:13; then A22: max- h is nonnegative by SUPINF_2:52; A23: max (K1,1) >= K1 by XXREAL_0:25; A24: for n being Nat for x being set st x in dom (F . 0) holds |.((F . n) . x).| <= max (K1,1) proof let n be Nat; ::_thesis: for x being set st x in dom (F . 0) holds |.((F . n) . x).| <= max (K1,1) let x be set ; ::_thesis: ( x in dom (F . 0) implies |.((F . n) . x).| <= max (K1,1) ) assume x in dom (F . 0) ; ::_thesis: |.((F . n) . x).| <= max (K1,1) then |.((F . n) . x).| <= K1 by A6; hence |.((F . n) . x).| <= max (K1,1) by A23, XXREAL_0:2; ::_thesis: verum end; A25: for x being Element of X for n being Nat st x in E holds |.(F . n).| . x <= h . x proof let x be Element of X; ::_thesis: for n being Nat st x in E holds |.(F . n).| . x <= h . x let n be Nat; ::_thesis: ( x in E implies |.(F . n).| . x <= h . x ) assume A26: x in E ; ::_thesis: |.(F . n).| . x <= h . x dom (F . n) = dom |.(F . n).| by MESFUNC1:def_10; then x in dom |.(F . n).| by A2, A26, MESFUNC8:def_2; then A27: |.(F . n).| . x = |.((F . n) . x).| by MESFUNC1:def_10; |.((F . n) . x).| <= max (K1,1) by A2, A24, A26; hence |.(F . n).| . x <= h . x by A9, A26, A27; ::_thesis: verum end; for x being set st x in dom (max+ h) holds 0. <= (max+ h) . x by MESFUNC2:12; then A28: max+ h is nonnegative by SUPINF_2:52; then A29: dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A22, MESFUNC5:22; A30: dom (max- h) = dom h by MESFUNC2:def_3; then A31: (max- h) | E = max- h by A8, RELAT_1:68; max- h is_measurable_on E by A7, A8, MESFUNC2:26, MESFUNC2:34; then ex C being Element of S st ( C = dom ((max+ h) + (max- h)) & integral+ (M,((max+ h) + (max- h))) = (integral+ (M,((max+ h) | C))) + (integral+ (M,((max- h) | C))) ) by A8, A19, A30, A21, A28, A22, MESFUNC5:78; then A32: (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) < +infty by A8, A19, A30, A29, A20, A31, A18, MESFUNC2:24; A33: for x being Element of X st x in dom (lim F) holds (lim F) . x = (lim_inf F) . x proof let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim_inf F) . x ) assume A34: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim_inf F) . x then x in E by A2, MESFUNC8:def_9; then F # x is convergent by A5; hence (lim F) . x = (lim_inf F) . x by A34, MESFUNC8:14; ::_thesis: verum end; A35: dom (lim_inf F) = dom (F . 0) by MESFUNC8:def_7; A36: h is_measurable_on E by A7, MESFUNC2:34; then 0 <= integral+ (M,(max- h)) by A8, A30, A22, MESFUNC2:26, MESFUNC5:79; then integral+ (M,(max+ h)) <> +infty by A32, XXREAL_3:def_2; then A37: integral+ (M,(max+ h)) < +infty by XXREAL_0:4; 0 <= integral+ (M,(max+ h)) by A8, A36, A19, A28, MESFUNC2:25, MESFUNC5:79; then integral+ (M,(max- h)) <> +infty by A32, XXREAL_3:def_2; then integral+ (M,(max- h)) < +infty by XXREAL_0:4; then A38: h is_integrable_on M by A8, A36, A37, MESFUNC5:def_17; then A39: ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & lim_inf I >= Integral (M,(lim_inf F)) & lim_sup I <= Integral (M,(lim_sup F)) & ( ( for x being Element of X st x in E holds F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) ) by A2, A3, A8, A13, A25, Th17; A40: now__::_thesis:_for_n_being_Nat_holds_F_._n_is_integrable_on_M let n be Nat; ::_thesis: F . n is_integrable_on M A41: E = dom (F . n) by A2, MESFUNC8:def_2; A42: F . n is_measurable_on E by A3; |.(F . n).| is_integrable_on M by A2, A3, A8, A38, A25, Th16; hence F . n is_integrable_on M by A41, A42, MESFUNC5:100; ::_thesis: verum end; A43: |.(lim_inf F).| is_integrable_on M by A2, A3, A8, A38, A25, Th16; dom (lim F) = dom (F . 0) by MESFUNC8:def_9; then A44: lim F = lim_inf F by A35, A33, PARTFUN1:5; then lim F is_measurable_on E by A2, A3, MESFUNC8:24; hence ( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,(lim F)) ) ) by A2, A5, A43, A40, A35, A44, A39, MESFUNC5:100; ::_thesis: verum end; definition let X be set ; let F be Functional_Sequence of X,ExtREAL; let f be PartFunc of X,ExtREAL; predF is_uniformly_convergent_to f means :Def2: :: MESFUN10:def 2 ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds ex N being Nat st for n being Nat for x being set st n >= N & x in dom (F . 0) holds |.(((F . n) . x) - (f . x)).| < e ) ); end; :: deftheorem Def2 defines is_uniformly_convergent_to MESFUN10:def_2_:_ for X being set for F being Functional_Sequence of X,ExtREAL for f being PartFunc of X,ExtREAL holds ( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being real number st e > 0 holds ex N being Nat st for n being Nat for x being set st n >= N & x in dom (F . 0) holds |.(((F . n) . x) - (f . x)).| < e ) ) ); theorem Th20: :: MESFUN10:20 for X being non empty set for F1 being Functional_Sequence of X,ExtREAL for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds for x being Element of X st x in dom (F1 . 0) holds ( F1 # x is convergent & lim (F1 # x) = f . x ) proof let X be non empty set ; ::_thesis: for F1 being Functional_Sequence of X,ExtREAL for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds for x being Element of X st x in dom (F1 . 0) holds ( F1 # x is convergent & lim (F1 # x) = f . x ) let F1 be Functional_Sequence of X,ExtREAL; ::_thesis: for f being PartFunc of X,ExtREAL st F1 is_uniformly_convergent_to f holds for x being Element of X st x in dom (F1 . 0) holds ( F1 # x is convergent & lim (F1 # x) = f . x ) let f be PartFunc of X,ExtREAL; ::_thesis: ( F1 is_uniformly_convergent_to f implies for x being Element of X st x in dom (F1 . 0) holds ( F1 # x is convergent & lim (F1 # x) = f . x ) ) assume A1: F1 is_uniformly_convergent_to f ; ::_thesis: for x being Element of X st x in dom (F1 . 0) holds ( F1 # x is convergent & lim (F1 # x) = f . x ) let x be Element of X; ::_thesis: ( x in dom (F1 . 0) implies ( F1 # x is convergent & lim (F1 # x) = f . x ) ) assume A2: x in dom (F1 . 0) ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x ) percases ( f . x in REAL or f . x = +infty or f . x = -infty ) by XXREAL_0:14; suppose f . x in REAL ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x ) then reconsider g = f . x as real number ; A3: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_N_being_Nat_st_ for_m_being_Nat_st_N_<=_m_holds_ |.(((F1_#_x)_._m)_-_(R_EAL_g)).|_<_e let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st for m being Nat st N <= m holds |.(((F1 # x) . m) - (R_EAL g)).| < e ) assume 0 < e ; ::_thesis: ex N being Nat st for m being Nat st N <= m holds |.(((F1 # x) . m) - (R_EAL g)).| < e then consider N being Nat such that A4: for n being Nat for x being set st n >= N & x in dom (F1 . 0) holds |.(((F1 . n) . x) - (f . x)).| < e by A1, Def2; take N = N; ::_thesis: for m being Nat st N <= m holds |.(((F1 # x) . m) - (R_EAL g)).| < e hereby ::_thesis: verum let m be Nat; ::_thesis: ( N <= m implies |.(((F1 # x) . m) - (R_EAL g)).| < e ) assume N <= m ; ::_thesis: |.(((F1 # x) . m) - (R_EAL g)).| < e then |.(((F1 . m) . x) - (f . x)).| < e by A2, A4; hence |.(((F1 # x) . m) - (R_EAL g)).| < e by MESFUNC5:def_13; ::_thesis: verum end; end; then A5: F1 # x is convergent_to_finite_number by MESFUNC5:def_8; then F1 # x is convergent by MESFUNC5:def_11; hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A3, A5, MESFUNC5:def_12; ::_thesis: verum end; supposeA6: f . x = +infty ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x ) now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_N_being_Nat_st_ for_n_being_Nat_st_n_>=_N_holds_ e_<=_(F1_#_x)_._n let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st for n being Nat st n >= N holds e <= (F1 # x) . n ) assume 0 < e ; ::_thesis: ex N being Nat st for n being Nat st n >= N holds e <= (F1 # x) . n then consider N being Nat such that A7: for n being Nat for x being set st n >= N & x in dom (F1 . 0) holds |.(((F1 . n) . x) - (f . x)).| < e by A1, Def2; take N = N; ::_thesis: for n being Nat st n >= N holds e <= (F1 # x) . n hereby ::_thesis: verum let n be Nat; ::_thesis: ( n >= N implies e <= (F1 # x) . n ) assume n >= N ; ::_thesis: e <= (F1 # x) . n then |.(((F1 . n) . x) - (f . x)).| < e by A2, A7; then A8: |.(- (((F1 . n) . x) - (f . x))).| < e by EXTREAL2:18; (F1 . n) . x = (F1 # x) . n by MESFUNC5:def_13; then - (((F1 # x) . n) - (f . x)) < R_EAL e by A8, EXTREAL2:10; then (f . x) - ((F1 # x) . n) < R_EAL e by XXREAL_3:26; then (F1 # x) . n = +infty by A6, XXREAL_3:54; hence e <= (F1 # x) . n by XXREAL_0:3; ::_thesis: verum end; end; then A9: F1 # x is convergent_to_+infty by MESFUNC5:def_9; then F1 # x is convergent by MESFUNC5:def_11; hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A6, A9, MESFUNC5:def_12; ::_thesis: verum end; supposeA10: f . x = -infty ; ::_thesis: ( F1 # x is convergent & lim (F1 # x) = f . x ) now__::_thesis:_for_e_being_real_number_st_e_<_0_holds_ ex_N_being_Nat_st_ for_n_being_Nat_st_n_>=_N_holds_ e_>=_(F1_#_x)_._n let e be real number ; ::_thesis: ( e < 0 implies ex N being Nat st for n being Nat st n >= N holds e >= (F1 # x) . n ) assume e < 0 ; ::_thesis: ex N being Nat st for n being Nat st n >= N holds e >= (F1 # x) . n then - 0 < - e by XREAL_1:24; then consider N being Nat such that A11: for n being Nat for x being set st n >= N & x in dom (F1 . 0) holds |.(((F1 . n) . x) - (f . x)).| < - e by A1, Def2; take N = N; ::_thesis: for n being Nat st n >= N holds e >= (F1 # x) . n hereby ::_thesis: verum let n be Nat; ::_thesis: ( n >= N implies e >= (F1 # x) . n ) assume n >= N ; ::_thesis: e >= (F1 # x) . n then A12: |.(((F1 . n) . x) - (f . x)).| < - e by A2, A11; (F1 . n) . x = (F1 # x) . n by MESFUNC5:def_13; then ((F1 # x) . n) - (f . x) < R_EAL (- e) by A12, EXTREAL2:10; then (F1 # x) . n = -infty by A10, XXREAL_3:54; hence e >= (F1 # x) . n by XXREAL_0:5; ::_thesis: verum end; end; then A13: F1 # x is convergent_to_-infty by MESFUNC5:def_10; then F1 # x is convergent by MESFUNC5:def_11; hence ( F1 # x is convergent & lim (F1 # x) = f . x ) by A10, A13, MESFUNC5:def_12; ::_thesis: verum end; end; end; theorem :: MESFUN10:21 for X being non empty set for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) proof let X be non empty set ; ::_thesis: for F being with_the_same_dom Functional_Sequence of X,ExtREAL for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) let F be with_the_same_dom Functional_Sequence of X,ExtREAL; ::_thesis: for S being SigmaField of X for M being sigma_Measure of S for E being Element of S for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) let S be SigmaField of X; ::_thesis: for M being sigma_Measure of S for E being Element of S for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) let M be sigma_Measure of S; ::_thesis: for E being Element of S for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) let E be Element of S; ::_thesis: for f being PartFunc of X,ExtREAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) let f be PartFunc of X,ExtREAL; ::_thesis: ( M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f implies ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) ) assume that A1: M . E < +infty and A2: E = dom (F . 0) and A3: for n being Nat holds F . n is_integrable_on M and A4: F is_uniformly_convergent_to f ; ::_thesis: ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) consider N being Nat such that A5: for n being Nat for x being set st n >= N & x in dom (F . 0) holds |.(((F . n) . x) - (f . x)).| < 1 / 2 by A4, Def2; reconsider N1 = N as Element of NAT by ORDINAL1:def_12; consider h being PartFunc of X,ExtREAL such that A6: h is_simple_func_in S and A7: dom h = E and A8: for x being set st x in E holds h . x = 1. by MESFUNC5:41; A9: max- h is_measurable_on E by A6, A7, MESFUNC2:26, MESFUNC2:34; for x being set st x in E holds h . x >= 0. by A8; then A10: h is nonnegative by A7, SUPINF_2:52; then A11: Integral (M,h) = integral' (M,h) by A6, MESFUNC5:89; set AFN = |.(F . N).|; A12: dom (F . N) = dom |.(F . N).| by MESFUNC1:def_10; now__::_thesis:_for_x_being_set_st_x_in_dom_|.(F_._N).|_holds_ 0_<=_|.(F_._N).|_._x let x be set ; ::_thesis: ( x in dom |.(F . N).| implies 0 <= |.(F . N).| . x ) assume x in dom |.(F . N).| ; ::_thesis: 0 <= |.(F . N).| . x then |.(F . N).| . x = |.((F . N) . x).| by MESFUNC1:def_10; hence 0 <= |.(F . N).| . x by EXTREAL2:3; ::_thesis: verum end; then A13: |.(F . N).| is nonnegative by SUPINF_2:52; then A14: dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, MESFUNC5:22; A15: for x being set st x in dom (F . 0) holds |.(((F . N) . x) - (f . x)).| < 1 / 2 by A5; A16: now__::_thesis:_for_x_being_set_ for_n_being_Nat_st_n_>=_N_&_x_in_dom_(F_._0)_holds_ |.(F_._n).|_._x_<=_(|.(F_._N).|_+_h)_._x let x be set ; ::_thesis: for n being Nat st n >= N & x in dom (F . 0) holds |.(F . n).| . x <= (|.(F . N).| + h) . x let n be Nat; ::_thesis: ( n >= N & x in dom (F . 0) implies |.(F . n).| . x <= (|.(F . N).| + h) . x ) assume that A17: n >= N and A18: x in dom (F . 0) ; ::_thesis: |.(F . n).| . x <= (|.(F . N).| + h) . x A19: |.(((F . n) . x) - (f . x)).| < 1 / 2 by A5, A17, A18; A20: |.(((F . N) . x) - (f . x)).| < 1 / 2 by A5, A18; A21: now__::_thesis:_(_(_f_._x_=_+infty_or_f_._x_=_-infty_)_implies_|.((F_._n)_._x).|_<=_|.((F_._N)_._x).|_+_1._) A22: |.(((F . n) . x) - (f . x)).| < 1. by A19, XXREAL_0:2; then A23: ((F . n) . x) - (f . x) < 1. by EXTREAL2:10; A24: |.(((F . N) . x) - (f . x)).| < 1. by A20, XXREAL_0:2; then A25: - 1. < ((F . N) . x) - (f . x) by EXTREAL2:10; A26: ((F . N) . x) - (f . x) < 1. by A24, EXTREAL2:10; assume A27: ( f . x = +infty or f . x = -infty ) ; ::_thesis: |.((F . n) . x).| <= |.((F . N) . x).| + 1. - 1. < ((F . n) . x) - (f . x) by A22, EXTREAL2:10; then ( ( (F . n) . x = +infty & (F . N) . x = +infty ) or ( (F . n) . x = -infty & (F . N) . x = -infty ) ) by A27, A25, A23, A26, XXREAL_3:53, XXREAL_3:54; hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by EXTREAL2:19, XXREAL_3:52; ::_thesis: verum end; dom (|.(F . N).| + h) = (dom |.(F . N).|) /\ (dom h) by A10, A13, MESFUNC5:22; then dom (|.(F . N).| + h) = E /\ E by A2, A7, A12, MESFUNC8:def_2; then (|.(F . N).| . x) + (h . x) = (|.(F . N).| + h) . x by A2, A18, MESFUNC1:def_3; then A28: (|.(F . N).| . x) + 1. = (|.(F . N).| + h) . x by A2, A8, A18; dom (F . n) = E by A2, MESFUNC8:def_2; then A29: x in dom |.(F . n).| by A2, A18, MESFUNC1:def_10; A30: now__::_thesis:_(_f_._x_in_REAL_implies_|.((F_._n)_._x).|_<=_|.((F_._N)_._x).|_+_1._) A31: 0 <= |.(((F . n) . x) - (f . x)).| by EXTREAL2:3; |.(((F . n) . x) - (f . x)).| < +infty by A19, XXREAL_0:2, XXREAL_0:9; then reconsider a = |.(((F . n) . x) - (f . x)).| as Real by A31, XXREAL_0:14; |.((f . x) - ((F . N) . x)).| < 1 / 2 by A20, MESFUNC5:1; then A32: |.((f . x) - ((F . N) . x)).| < +infty by XXREAL_0:2, XXREAL_0:9; 0 <= |.((f . x) - ((F . N) . x)).| by EXTREAL2:3; then reconsider b = |.((f . x) - ((F . N) . x)).| as Real by A32, XXREAL_0:14; assume A33: f . x in REAL ; ::_thesis: |.((F . n) . x).| <= |.((F . N) . x).| + 1. A34: now__::_thesis:_(_not_(F_._N)_._x_=_+infty_&_not_(F_._N)_._x_=_-infty_) assume ( (F . N) . x = +infty or (F . N) . x = -infty ) ; ::_thesis: contradiction then ( ((F . N) . x) - (f . x) = +infty or ((F . N) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14; then 1. < |.(((F . N) . x) - (f . x)).| by EXTREAL2:19, XXREAL_0:9; hence contradiction by A15, A18, XXREAL_0:2; ::_thesis: verum end; A35: now__::_thesis:_(_not_(F_._n)_._x_=_+infty_&_not_(F_._n)_._x_=_-infty_) assume ( (F . n) . x = +infty or (F . n) . x = -infty ) ; ::_thesis: contradiction then ( ((F . n) . x) - (f . x) = +infty or ((F . n) . x) - (f . x) = -infty ) by A33, XXREAL_3:13, XXREAL_3:14; hence contradiction by A19, EXTREAL2:19, XXREAL_0:9; ::_thesis: verum end; then (F . n) . x in REAL by XXREAL_0:14; then A36: |.((F . n) . x).| - |.((F . N) . x).| <= |.(((F . n) . x) - ((F . N) . x)).| by EXTREAL2:20; b <= 1 / 2 by A20, MESFUNC5:1; then a + b < (1 / 2) + (1 / 2) by A19, XREAL_1:8; then A37: |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| < 1 by SUPINF_2:1; (- (f . x)) + (f . x) = 0. by XXREAL_3:7; then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) + ((- (f . x)) + (f . x))) - ((F . N) . x) by XXREAL_3:4; then ((F . n) . x) - ((F . N) . x) = ((((F . n) . x) + (- (f . x))) + (f . x)) - ((F . N) . x) by A33, A35, XXREAL_3:29; then ((F . n) . x) - ((F . N) . x) = (((F . n) . x) - (f . x)) + ((f . x) - ((F . N) . x)) by A33, A34, XXREAL_3:30; then |.(((F . n) . x) - ((F . N) . x)).| <= |.(((F . n) . x) - (f . x)).| + |.((f . x) - ((F . N) . x)).| by EXTREAL2:13; then |.(((F . n) . x) - ((F . N) . x)).| < 1 by A37, XXREAL_0:2; then |.((F . n) . x).| - |.((F . N) . x).| <= 1. by A36, XXREAL_0:2; hence |.((F . n) . x).| <= |.((F . N) . x).| + 1. by XXREAL_3:52; ::_thesis: verum end; x in dom |.(F . N).| by A12, A18, MESFUNC8:def_2; then |.((F . n) . x).| <= (|.(F . N).| . x) + 1. by A30, A21, MESFUNC1:def_10, XXREAL_0:14; hence |.(F . n).| . x <= (|.(F . N).| + h) . x by A28, A29, MESFUNC1:def_10; ::_thesis: verum end; A38: for x being Element of X for n being Nat st x in E holds |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x proof let x be Element of X; ::_thesis: for n being Nat st x in E holds |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x let n be Nat; ::_thesis: ( x in E implies |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x ) A39: (F ^\ N1) . n = F . (n + N) by NAT_1:def_3; assume x in E ; ::_thesis: |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x hence |.((F ^\ N1) . n).| . x <= (|.(F . N).| + h) . x by A2, A16, A39, NAT_1:11; ::_thesis: verum end; A40: max+ h is_measurable_on E by A6, MESFUNC2:25, MESFUNC2:34; for x being set st x in dom (max- h) holds 0. <= (max- h) . x by MESFUNC2:13; then A41: max- h is nonnegative by SUPINF_2:52; A42: for n being Nat holds F . n is_measurable_on E proof let n be Nat; ::_thesis: F . n is_measurable_on E F . n is_integrable_on M by A3; then ex A being Element of S st ( A = dom (F . n) & F . n is_measurable_on A ) by MESFUNC5:def_17; hence F . n is_measurable_on E by A2, MESFUNC8:def_2; ::_thesis: verum end; then A43: F . N is_measurable_on E ; (F ^\ N1) . 0 = F . (0 + N) by NAT_1:def_3; then A44: dom ((F ^\ N1) . 0) = E by A2, MESFUNC8:def_2; A45: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_f_holds_ (lim_F)_._x_=_f_._x let x be Element of X; ::_thesis: ( x in dom f implies (lim F) . x = f . x ) assume x in dom f ; ::_thesis: (lim F) . x = f . x then A46: x in dom (F . 0) by A4, Def2; then A47: x in dom (lim F) by MESFUNC8:def_9; lim (F # x) = f . x by A4, A46, Th20; hence (lim F) . x = f . x by A47, MESFUNC8:def_9; ::_thesis: verum end; dom f = dom (F . 0) by A4, Def2; then dom (lim F) = dom f by MESFUNC8:def_9; then A48: lim F = f by A45, PARTFUN1:5; A49: F . N is_integrable_on M by A3; E = dom (F . N) by A2, MESFUNC8:def_2; then A50: |.(F . N).| is_integrable_on M by A49, A43, MESFUNC5:100; deffunc H1( Element of NAT ) -> Element of ExtREAL = Integral (M,(F . \$1)); A51: (R_EAL 1) * +infty = +infty by XXREAL_3:def_5; A52: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_h_holds_ |.h.|_._x_=_h_._x let x be Element of X; ::_thesis: ( x in dom h implies |.h.| . x = h . x ) assume x in dom h ; ::_thesis: |.h.| . x = h . x then A53: x in dom |.h.| by MESFUNC1:def_10; 0 <= h . x by A10, SUPINF_2:51; then |.(h . x).| = h . x by EXTREAL1:def_1; hence |.h.| . x = h . x by A53, MESFUNC1:def_10; ::_thesis: verum end; dom h = dom |.h.| by MESFUNC1:def_10; then A54: h = |.h.| by A52, PARTFUN1:5; Integral (M,h) = integral+ (M,h) by A6, A10, MESFUNC5:89; then integral+ (M,h) = (R_EAL 1) * (M . (dom h)) by A7, A8, A11, MESFUNC5:104; then A55: integral+ (M,|.h.|) < +infty by A1, A7, A54, A51, XXREAL_3:72; A56: for n being Nat holds (F ^\ N1) . n is_measurable_on E proof let n be Nat; ::_thesis: (F ^\ N1) . n is_measurable_on E (F ^\ N1) . n = F . (n + N) by NAT_1:def_3; hence (F ^\ N1) . n is_measurable_on E by A42; ::_thesis: verum end; A57: for x being Element of X st x in E holds ( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) ) proof let x be Element of X; ::_thesis: ( x in E implies ( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) ) ) A58: now__::_thesis:_for_n_being_Element_of_NAT_holds_((F_^\_N1)_#_x)_._n_=_((F_#_x)_^\_N1)_._n let n be Element of NAT ; ::_thesis: ((F ^\ N1) # x) . n = ((F # x) ^\ N1) . n ((F ^\ N1) # x) . n = ((F ^\ N1) . n) . x by MESFUNC5:def_13; then ((F ^\ N1) # x) . n = (F . (n + N)) . x by NAT_1:def_3; then ((F ^\ N1) # x) . n = (F # x) . (n + N) by MESFUNC5:def_13; hence ((F ^\ N1) # x) . n = ((F # x) ^\ N1) . n by NAT_1:def_3; ::_thesis: verum end; assume x in E ; ::_thesis: ( (F ^\ N1) # x is convergent & lim (F # x) = lim ((F ^\ N1) # x) ) then A59: F # x is convergent by A2, A4, Th20; then (F # x) ^\ N1 is convergent by RINFSUP2:21; hence (F ^\ N1) # x is convergent by A58, FUNCT_2:63; ::_thesis: lim (F # x) = lim ((F ^\ N1) # x) lim (F # x) = lim ((F # x) ^\ N1) by A59, RINFSUP2:21; hence lim (F # x) = lim ((F ^\ N1) # x) by A58, FUNCT_2:63; ::_thesis: verum end; then for x being Element of X st x in E holds (F ^\ N1) # x is convergent ; then A60: lim (F ^\ N1) is_measurable_on E by A56, A44, MESFUNC8:25; dom (lim (F ^\ N1)) = E by A44, MESFUNC8:def_9; then A61: dom (lim F) = dom (lim (F ^\ N1)) by A2, MESFUNC8:def_9; A62: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_F)_holds_ (lim_F)_._x_=_(lim_(F_^\_N1))_._x let x be Element of X; ::_thesis: ( x in dom (lim F) implies (lim F) . x = (lim (F ^\ N1)) . x ) assume A63: x in dom (lim F) ; ::_thesis: (lim F) . x = (lim (F ^\ N1)) . x then x in E by A2, MESFUNC8:def_9; then A64: lim (F # x) = lim ((F ^\ N1) # x) by A57; lim ((F ^\ N1) # x) = (lim (F ^\ N1)) . x by A61, A63, MESFUNC8:def_9; hence (lim F) . x = (lim (F ^\ N1)) . x by A63, A64, MESFUNC8:def_9; ::_thesis: verum end; A65: dom (max- h) = dom h by MESFUNC2:def_3; then A66: (max- h) | E = max- h by A7, RELAT_1:68; A67: dom (max+ h) = dom h by MESFUNC2:def_2; then A68: (max+ h) | E = max+ h by A7, RELAT_1:68; for x being set st x in dom (max+ h) holds 0. <= (max+ h) . x by MESFUNC2:12; then A69: max+ h is nonnegative by SUPINF_2:52; then dom ((max+ h) + (max- h)) = (dom (max+ h)) /\ (dom (max- h)) by A41, MESFUNC5:22; then ex C being Element of S st ( C = E & integral+ (M,((max+ h) + (max- h))) = (integral+ (M,((max+ h) | C))) + (integral+ (M,((max- h) | C))) ) by A7, A40, A9, A69, A41, A67, A65, MESFUNC5:78; then A70: integral+ (M,|.h.|) = (integral+ (M,(max+ h))) + (integral+ (M,(max- h))) by A68, A66, MESFUNC2:24; A71: h is_measurable_on E by A6, MESFUNC2:34; then 0 <= integral+ (M,(max- h)) by A7, A41, A65, MESFUNC2:26, MESFUNC5:79; then integral+ (M,(max+ h)) <> +infty by A70, A55, XXREAL_3:def_2; then A72: integral+ (M,(max+ h)) < +infty by XXREAL_0:4; 0 <= integral+ (M,(max+ h)) by A7, A71, A69, A67, MESFUNC2:25, MESFUNC5:79; then integral+ (M,(max- h)) <> +infty by A70, A55, XXREAL_3:def_2; then integral+ (M,(max- h)) < +infty by XXREAL_0:4; then h is_integrable_on M by A7, A71, A72, MESFUNC5:def_17; then A73: |.(F . N).| + h is_integrable_on M by A50, MESFUNC5:108; A74: E = dom |.(F . N).| by A2, A12, MESFUNC8:def_2; then A75: |.(lim_inf (F ^\ N1)).| is_integrable_on M by A7, A73, A14, A38, A56, A44, Th16; |.(F . N).| + h is nonnegative by A10, A13, MESFUNC5:22; then consider J being ExtREAL_sequence such that A76: for n being Nat holds J . n = Integral (M,((F ^\ N1) . n)) and lim_inf J >= Integral (M,(lim_inf (F ^\ N1))) and lim_sup J <= Integral (M,(lim_sup (F ^\ N1))) and A77: ( ( for x being Element of X st x in E holds (F ^\ N1) # x is convergent ) implies ( J is convergent & lim J = Integral (M,(lim (F ^\ N1))) ) ) by A7, A73, A14, A74, A38, A56, A44, Th17; consider I being Function of NAT,ExtREAL such that A78: for n being Element of NAT holds I . n = H1(n) from FUNCT_2:sch_4(); reconsider I = I as ExtREAL_sequence ; A79: dom (lim_inf (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def_7; A80: now__::_thesis:_for_x_being_Element_of_X_st_x_in_dom_(lim_(F_^\_N1))_holds_ (lim_(F_^\_N1))_._x_=_(lim_inf_(F_^\_N1))_._x let x be Element of X; ::_thesis: ( x in dom (lim (F ^\ N1)) implies (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x ) assume A81: x in dom (lim (F ^\ N1)) ; ::_thesis: (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x then x in E by A44, MESFUNC8:def_9; then (F ^\ N1) # x is convergent by A57; hence (lim (F ^\ N1)) . x = (lim_inf (F ^\ N1)) . x by A81, MESFUNC8:14; ::_thesis: verum end; dom (lim (F ^\ N1)) = dom ((F ^\ N1) . 0) by MESFUNC8:def_9; then lim (F ^\ N1) = lim_inf (F ^\ N1) by A79, A80, PARTFUN1:5; then A82: lim (F ^\ N1) is_integrable_on M by A44, A75, A79, A60, MESFUNC5:100; A83: for n being Nat holds I . n = Integral (M,(F . n)) proof let n be Nat; ::_thesis: I . n = Integral (M,(F . n)) n is Element of NAT by ORDINAL1:def_12; hence I . n = Integral (M,(F . n)) by A78; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_J_._n_=_(I_^\_N1)_._n let n be Element of NAT ; ::_thesis: J . n = (I ^\ N1) . n A84: (F ^\ N1) . n = F . (n + N) by NAT_1:def_3; A85: (I ^\ N1) . n = I . (n + N) by NAT_1:def_3; J . n = Integral (M,((F ^\ N1) . n)) by A76; hence J . n = (I ^\ N1) . n by A78, A84, A85; ::_thesis: verum end; then A86: J = I ^\ N1 by FUNCT_2:63; then A87: I is convergent by A57, A77, RINFSUP2:17; lim I = lim J by A57, A77, A86, RINFSUP2:17; then lim I = Integral (M,(lim F)) by A57, A61, A62, A77, PARTFUN1:5; hence ( f is_integrable_on M & ex I being ExtREAL_sequence st ( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & lim I = Integral (M,f) ) ) by A48, A61, A62, A82, A83, A87, PARTFUN1:5; ::_thesis: verum end;