let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) implies ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I ) )

assume that

A1: E = dom (F . 0) and

A2: F . 0 is nonpositive and

A3: F is with_the_same_dom and

A4: for n being Nat holds F . n is E -measurable and

A5: for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x and

A6: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

set G = - F;

A7: (- F) . 0 = - (F . 0) by Th37;

then A8: E = dom ((- F) . 0) by A1, MESFUNC1:def 7;

A11: for n being Nat holds (- F) . n is E -measurable

for x being Element of X st x in E holds

((- F) . n) . x <= ((- F) . m) . x

(- F) # x is convergent

A19: ( ( for n being Nat holds J . n = Integral (M,((- F) . n)) ) & J is convergent & Integral (M,(lim (- F))) = lim J ) by A8, A2, A7, A3, Th40, A11, A13, A18, MESFUNC9:52;

set I = - J;

take - J ; :: thesis: ( ( for n being Nat holds (- J) . n = Integral (M,(F . n)) ) & - J is convergent & Integral (M,(lim F)) = lim (- J) )

thus for n being Nat holds (- J) . n = Integral (M,(F . n)) :: thesis: ( - J is convergent & Integral (M,(lim F)) = lim (- J) )

A23: lim (- J) = - (Integral (M,(lim (- F)))) by A19, DBLSEQ_3:17;

A24: E = dom (lim F) by A1, MESFUNC8:def 9;

then A25: dom (- (lim F)) = E by MESFUNC1:def 7;

then A26: dom (lim (- F)) = dom (- (lim F)) by A8, MESFUNC8:def 9;

for x being Element of X st x in dom (lim (- F)) holds

(lim (- F)) . x = (- (lim F)) . x

then Integral (M,(lim (- F))) = - (Integral (M,(lim F))) by A1, A3, A4, A6, A24, Th52, MESFUNC8:25;

hence Integral (M,(lim F)) = lim (- J) by A23; :: thesis: verum

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let M be sigma_Measure of S; :: thesis: for F being Functional_Sequence of X,ExtREAL

for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let F be Functional_Sequence of X,ExtREAL; :: thesis: for E being Element of S st E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

let E be Element of S; :: thesis: ( E = dom (F . 0) & F . 0 is nonpositive & F is with_the_same_dom & ( for n being Nat holds F . n is E -measurable ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) implies ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I ) )

assume that

A1: E = dom (F . 0) and

A2: F . 0 is nonpositive and

A3: F is with_the_same_dom and

A4: for n being Nat holds F . n is E -measurable and

A5: for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x >= (F . m) . x and

A6: for x being Element of X st x in E holds

F # x is convergent ; :: thesis: ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

set G = - F;

A7: (- F) . 0 = - (F . 0) by Th37;

then A8: E = dom ((- F) . 0) by A1, MESFUNC1:def 7;

A11: for n being Nat holds (- F) . n is E -measurable

proof

A13:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: (- F) . n is E -measurable

E = dom (F . n) by A1, A3, MESFUNC8:def 2;

then - (F . n) is E -measurable by A4, MEASUR11:63;

hence (- F) . n is E -measurable by Th37; :: thesis: verum

end;E = dom (F . n) by A1, A3, MESFUNC8:def 2;

then - (F . n) is E -measurable by A4, MEASUR11:63;

hence (- F) . n is E -measurable by Th37; :: thesis: verum

for x being Element of X st x in E holds

((- F) . n) . x <= ((- F) . m) . x

proof

A18:
for x being Element of X st x in E holds
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in E holds

((- F) . n) . x <= ((- F) . m) . x )

assume A14: n <= m ; :: thesis: for x being Element of X st x in E holds

((- F) . n) . x <= ((- F) . m) . x

let x be Element of X; :: thesis: ( x in E implies ((- F) . n) . x <= ((- F) . m) . x )

assume A15: x in E ; :: thesis: ((- F) . n) . x <= ((- F) . m) . x

then A17: ( x in dom ((- F) . n) & x in dom ((- F) . m) ) by A8, A3, Th40, MESFUNC8:def 2;

( (- F) . n = - (F . n) & (- F) . m = - (F . m) ) by Th37;

then ( ((- F) . n) . x = - ((F . n) . x) & ((- F) . m) . x = - ((F . m) . x) ) by A17, MESFUNC1:def 7;

hence ((- F) . n) . x <= ((- F) . m) . x by A15, A5, A14, XXREAL_3:38; :: thesis: verum

end;((- F) . n) . x <= ((- F) . m) . x )

assume A14: n <= m ; :: thesis: for x being Element of X st x in E holds

((- F) . n) . x <= ((- F) . m) . x

let x be Element of X; :: thesis: ( x in E implies ((- F) . n) . x <= ((- F) . m) . x )

assume A15: x in E ; :: thesis: ((- F) . n) . x <= ((- F) . m) . x

then A17: ( x in dom ((- F) . n) & x in dom ((- F) . m) ) by A8, A3, Th40, MESFUNC8:def 2;

( (- F) . n = - (F . n) & (- F) . m = - (F . m) ) by Th37;

then ( ((- F) . n) . x = - ((F . n) . x) & ((- F) . m) . x = - ((F . m) . x) ) by A17, MESFUNC1:def 7;

hence ((- F) . n) . x <= ((- F) . m) . x by A15, A5, A14, XXREAL_3:38; :: thesis: verum

(- F) # x is convergent

proof

consider J being ExtREAL_sequence such that
let x be Element of X; :: thesis: ( x in E implies (- F) # x is convergent )

assume x in E ; :: thesis: (- F) # x is convergent

then F # x is convergent by A6;

then - (F # x) is convergent by DBLSEQ_3:17;

hence (- F) # x is convergent by Th38; :: thesis: verum

end;assume x in E ; :: thesis: (- F) # x is convergent

then F # x is convergent by A6;

then - (F # x) is convergent by DBLSEQ_3:17;

hence (- F) # x is convergent by Th38; :: thesis: verum

A19: ( ( for n being Nat holds J . n = Integral (M,((- F) . n)) ) & J is convergent & Integral (M,(lim (- F))) = lim J ) by A8, A2, A7, A3, Th40, A11, A13, A18, MESFUNC9:52;

set I = - J;

take - J ; :: thesis: ( ( for n being Nat holds (- J) . n = Integral (M,(F . n)) ) & - J is convergent & Integral (M,(lim F)) = lim (- J) )

thus for n being Nat holds (- J) . n = Integral (M,(F . n)) :: thesis: ( - J is convergent & Integral (M,(lim F)) = lim (- J) )

proof

thus
- J is convergent
by A19, DBLSEQ_3:17; :: thesis: Integral (M,(lim F)) = lim (- J)
let n be Nat; :: thesis: (- J) . n = Integral (M,(F . n))

n in NAT by ORDINAL1:def 12;

then A20: n in dom (- J) by FUNCT_2:def 1;

A21: dom (F . n) = E by A1, A3, MESFUNC8:def 2;

(- F) . n = - (F . n) by Th37;

then Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by A21, A4, Th52;

then J . n = - (Integral (M,(F . n))) by A19;

then (- J) . n = - (- (Integral (M,(F . n)))) by A20, MESFUNC1:def 7;

hence (- J) . n = Integral (M,(F . n)) ; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then A20: n in dom (- J) by FUNCT_2:def 1;

A21: dom (F . n) = E by A1, A3, MESFUNC8:def 2;

(- F) . n = - (F . n) by Th37;

then Integral (M,((- F) . n)) = - (Integral (M,(F . n))) by A21, A4, Th52;

then J . n = - (Integral (M,(F . n))) by A19;

then (- J) . n = - (- (Integral (M,(F . n)))) by A20, MESFUNC1:def 7;

hence (- J) . n = Integral (M,(F . n)) ; :: thesis: verum

A23: lim (- J) = - (Integral (M,(lim (- F)))) by A19, DBLSEQ_3:17;

A24: E = dom (lim F) by A1, MESFUNC8:def 9;

then A25: dom (- (lim F)) = E by MESFUNC1:def 7;

then A26: dom (lim (- F)) = dom (- (lim F)) by A8, MESFUNC8:def 9;

for x being Element of X st x in dom (lim (- F)) holds

(lim (- F)) . x = (- (lim F)) . x

proof

then
lim (- F) = - (lim F)
by A26, PARTFUN1:5;
let x be Element of X; :: thesis: ( x in dom (lim (- F)) implies (lim (- F)) . x = (- (lim F)) . x )

assume A27: x in dom (lim (- F)) ; :: thesis: (lim (- F)) . x = (- (lim F)) . x

then A30: (lim (- F)) . x = lim ((- F) # x) by MESFUNC8:def 9;

A28: F # x is convergent by A27, A26, A25, A6;

(- F) # x = - (F # x) by Th38;

then A29: lim ((- F) # x) = - (lim (F # x)) by A28, DBLSEQ_3:17;

lim (F # x) = (lim F) . x by A27, A26, A25, A24, MESFUNC8:def 9;

hence (lim (- F)) . x = (- (lim F)) . x by A29, A30, A27, A26, MESFUNC1:def 7; :: thesis: verum

end;assume A27: x in dom (lim (- F)) ; :: thesis: (lim (- F)) . x = (- (lim F)) . x

then A30: (lim (- F)) . x = lim ((- F) # x) by MESFUNC8:def 9;

A28: F # x is convergent by A27, A26, A25, A6;

(- F) # x = - (F # x) by Th38;

then A29: lim ((- F) # x) = - (lim (F # x)) by A28, DBLSEQ_3:17;

lim (F # x) = (lim F) . x by A27, A26, A25, A24, MESFUNC8:def 9;

hence (lim (- F)) . x = (- (lim F)) . x by A29, A30, A27, A26, MESFUNC1:def 7; :: thesis: verum

then Integral (M,(lim (- F))) = - (Integral (M,(lim F))) by A1, A3, A4, A6, A24, Th52, MESFUNC8:25;

hence Integral (M,(lim F)) = lim (- J) by A23; :: thesis: verum