:: Integral of Non Positive Functions
:: by Noboru Endou
::
:: Received September 3, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


registration
let X be non empty set ;
let f be nonnegative PartFunc of X,ExtREAL;
cluster - f -> nonpositive ;
correctness
coherence
- f is nonpositive ;
proof end;
end;

registration
let X be non empty set ;
let f be nonpositive PartFunc of X,ExtREAL;
cluster - f -> nonnegative ;
correctness
coherence
- f is nonnegative ;
proof end;
end;

theorem Th1: :: MESFUN11:1
for X being non empty set
for f being nonpositive PartFunc of X,ExtREAL
for E being set holds f | E is nonpositive
proof end;

theorem Th2: :: MESFUN11:2
for X being non empty set
for A being set
for r being Real
for f being PartFunc of X,ExtREAL holds (r (#) f) | A = r (#) (f | A)
proof end;

theorem Th3: :: MESFUN11:3
for X being non empty set
for A being set
for f being PartFunc of X,ExtREAL holds - (f | A) = (- f) | A
proof end;

theorem Th4: :: MESFUN11:4
for X being non empty set
for f being PartFunc of X,ExtREAL
for c being Real st f is nonpositive holds
( ( 0 <= c implies c (#) f is nonpositive ) & ( c <= 0 implies c (#) f is nonnegative ) )
proof end;

theorem Th5: :: MESFUN11:5
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( max+ f is nonnegative & max- f is nonnegative & |.f.| is nonnegative )
proof end;

theorem :: MESFUN11:6
for X being non empty set
for f being PartFunc of X,ExtREAL
for x being object holds
( f . x <= (max+ f) . x & f . x >= - ((max- f) . x) )
proof end;

Lm1: for X being non empty set
for f being PartFunc of X,ExtREAL
for r being Real holds
( ( r > 0 implies less_dom (f,r) = less_dom ((max+ f),r) ) & ( r <= 0 implies less_dom (f,r) = great_dom ((max- f),(- r)) ) )
proof end;

theorem :: MESFUN11:7
for X being non empty set
for f being PartFunc of X,ExtREAL
for r being positive Real holds less_dom (f,r) = less_dom ((max+ f),r) by Lm1;

theorem :: MESFUN11:8
for X being non empty set
for f being PartFunc of X,ExtREAL
for r being non positive Real holds less_dom (f,r) = great_dom ((max- f),(- r)) by Lm1;

theorem Th9: :: MESFUN11:9
for X being non empty set
for f, g being PartFunc of X,ExtREAL
for a being ExtReal
for r being Real st r <> 0 & g = r (#) f holds
eq_dom (f,a) = eq_dom (g,(a * r))
proof end;

theorem Th10: :: MESFUN11:10
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st A c= dom f holds
( f is A -measurable iff ( max+ f is A -measurable & max- f is A -measurable ) )
proof end;

Lm2: for i, j being Nat st i <= j holds
ex k being Nat st j = i + k
proof end;

definition
let X be non empty set ;
let f be Function of X,ExtREAL;
let r be Real;
:: original: (#)
redefine func r (#) f -> Function of X,ExtREAL;
correctness
coherence
r (#) f is Function of X,ExtREAL;
proof end;
end;

theorem Th11: :: MESFUN11:11
for X being non empty set
for r being Real
for f being V121() Function of X,ExtREAL st r >= 0 holds
r (#) f is V121()
proof end;

registration
let X be non empty set ;
let f be V121() Function of X,ExtREAL;
let r be non negative Real;
cluster r (#) f -> V121() for Function of X,ExtREAL;
coherence
for b1 being Function of X,ExtREAL st b1 = r (#) f holds
b1 is without+infty by Th11;
end;

theorem Th12: :: MESFUN11:12
for X being non empty set
for r being Real
for f being V121() Function of X,ExtREAL st r <= 0 holds
r (#) f is V120()
proof end;

registration
let X be non empty set ;
let f be V121() Function of X,ExtREAL;
let r be non positive Real;
cluster r (#) f -> V120() ;
correctness
coherence
r (#) f is without-infty ;
by Th12;
end;

theorem Th13: :: MESFUN11:13
for X being non empty set
for r being Real
for f being V120() Function of X,ExtREAL st r >= 0 holds
r (#) f is V120()
proof end;

registration
let X be non empty set ;
let f be V120() Function of X,ExtREAL;
let r be non negative Real;
cluster r (#) f -> V120() ;
correctness
coherence
r (#) f is without-infty ;
by Th13;
end;

theorem Th14: :: MESFUN11:14
for X being non empty set
for r being Real
for f being V120() Function of X,ExtREAL st r <= 0 holds
r (#) f is V121()
proof end;

registration
let X be non empty set ;
let f be V120() Function of X,ExtREAL;
let r be non positive Real;
cluster r (#) f -> V121() ;
correctness
coherence
r (#) f is without+infty ;
by Th14;
end;

theorem Th15: :: MESFUN11:15
for X being non empty set
for r being Real
for f being V120() V121() Function of X,ExtREAL holds
( r (#) f is V120() & r (#) f is V121() )
proof end;

registration
let X be non empty set ;
let f be V120() V121() Function of X,ExtREAL;
let r be Real;
cluster r (#) f -> V120() V121() ;
correctness
coherence
( r (#) f is without-infty & r (#) f is without+infty );
by Th15;
end;

theorem Th16: :: MESFUN11:16
for X being non empty set
for r being positive Real
for f being Function of X,ExtREAL holds
( f is V121() iff r (#) f is V121() )
proof end;

theorem Th17: :: MESFUN11:17
for X being non empty set
for r being negative Real
for f being Function of X,ExtREAL holds
( f is V121() iff r (#) f is V120() )
proof end;

theorem Th18: :: MESFUN11:18
for X being non empty set
for r being positive Real
for f being Function of X,ExtREAL holds
( f is V120() iff r (#) f is V120() )
proof end;

theorem Th19: :: MESFUN11:19
for X being non empty set
for r being negative Real
for f being Function of X,ExtREAL holds
( f is V120() iff r (#) f is V121() )
proof end;

theorem :: MESFUN11:20
for X being non empty set
for r being non zero Real
for f being Function of X,ExtREAL holds
( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )
proof end;

theorem Th21: :: MESFUN11:21
for X, Y being non empty set
for f being PartFunc of X,ExtREAL
for r being Real st f = Y --> r holds
( f is V120() & f is V121() )
proof end;

theorem :: MESFUN11:22
for X being non empty set
for f being Function of X,ExtREAL holds
( 0 (#) f = X --> 0 & 0 (#) f is V120() & 0 (#) f is V121() )
proof end;

theorem Th23: :: MESFUN11:23
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & f is V121() holds
( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) & dom (g - f) = (dom f) /\ (dom g) )
proof end;

theorem :: MESFUN11:24
for X being non empty set
for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds
( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )
proof end;

theorem :: MESFUN11:25
for X being non empty set
for f1, f2 being Function of X,ExtREAL st f1 is V120() & f1 is V121() holds
( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )
proof end;

theorem :: MESFUN11:26
for X being non empty set
for f1, f2 being Function of X,ExtREAL st f2 is V120() & f2 is V121() holds
( f1 - f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 - f2) . x = (f1 . x) - (f2 . x) ) )
proof end;

theorem :: MESFUN11:27
for X, Y being non empty set
for f1, f2 being PartFunc of X,ExtREAL st dom f1 c= Y & f2 = Y --> 0 holds
( f1 + f2 = f1 & f1 - f2 = f1 & f2 - f1 = - f1 )
proof end;

theorem Th28: :: MESFUN11:28
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_simple_func_in S & g is_simple_func_in S holds
f + g is_simple_func_in S
proof end;

theorem :: MESFUN11:29
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_simple_func_in S & g is_simple_func_in S holds
f - g is_simple_func_in S
proof end;

theorem Th30: :: MESFUN11:30
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
- f is_simple_func_in S
proof end;

theorem :: MESFUN11:31
for X being non empty set
for f being nonnegative PartFunc of X,ExtREAL holds f = max+ f
proof end;

theorem Th32: :: MESFUN11:32
for X being non empty set
for f being nonpositive PartFunc of X,ExtREAL holds f = - (max- f)
proof end;

theorem Th33: :: MESFUN11:33
for C being non empty set
for f being PartFunc of C,ExtREAL
for c being Real st c <= 0 holds
( max+ (c (#) f) = (- c) (#) (max- f) & max- (c (#) f) = (- c) (#) (max+ f) )
proof end;

theorem Th34: :: MESFUN11:34
for X being non empty set
for f being PartFunc of X,ExtREAL holds max+ f = max- (- f)
proof end;

theorem Th35: :: MESFUN11:35
for X being non empty set
for f being PartFunc of X,ExtREAL
for r1, r2 being Real holds r1 (#) (r2 (#) f) = (r1 * r2) (#) f
proof end;

theorem Th36: :: MESFUN11:36
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f = - g holds
g = - f
proof end;

definition
let X be non empty set ;
let F be Functional_Sequence of X,ExtREAL;
let r be Real;
func r (#) F -> Functional_Sequence of X,ExtREAL means :Def1: :: MESFUN11:def 1
 for n being Nat holds it . n = r (#) (F . n);
existence
ex b1 being Functional_Sequence of X,ExtREAL st
for n being Nat holds b1 . n = r (#) (F . n)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X,ExtREAL st ( for n being Nat holds b1 . n = r (#) (F . n) ) & ( for n being Nat holds b2 . n = r (#) (F . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines (#) MESFUN11:def 1 :
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for r being Real
for b4 being Functional_Sequence of X,ExtREAL holds
( b4 = r (#) F iff for n being Nat holds b4 . n = r (#) (F . n) );

definition
let X be non empty set ;
let F be Functional_Sequence of X,ExtREAL;
func - F -> Functional_Sequence of X,ExtREAL equals :: MESFUN11:def 2
(- 1) (#) F;
correctness
coherence
(- 1) (#) F is Functional_Sequence of X,ExtREAL;
;
end;

:: deftheorem defines - MESFUN11:def 2 :
for X being non empty set
for F being Functional_Sequence of X,ExtREAL holds - F = (- 1) (#) F;

theorem Th37: :: MESFUN11:37
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat holds (- F) . n = - (F . n)
proof end;

theorem Th38: :: MESFUN11:38
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X holds (- F) # x = - (F # x)
proof end;

theorem Th39: :: MESFUN11:39
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X holds
( ( F # x is convergent_to_+infty implies (- F) # x is convergent_to_-infty ) & ( (- F) # x is convergent_to_-infty implies F # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies (- F) # x is convergent_to_+infty ) & ( (- F) # x is convergent_to_+infty implies F # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies (- F) # x is convergent_to_finite_number ) & ( (- F) # x is convergent_to_finite_number implies F # x is convergent_to_finite_number ) & ( F # x is convergent implies (- F) # x is convergent ) & ( (- F) # x is convergent implies F # x is convergent ) & ( F # x is convergent implies lim ((- F) # x) = - (lim (F # x)) ) )
proof end;

theorem Th40: :: MESFUN11:40
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st F is with_the_same_dom holds
- F is with_the_same_dom
proof end;

theorem Th41: :: MESFUN11:41
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st F is additive holds
- F is additive
proof end;

theorem Th42: :: MESFUN11:42
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat holds (Partial_Sums (- F)) . n = (- (Partial_Sums F)) . n
proof end;

theorem Th43: :: MESFUN11:43
for seq being ExtREAL_sequence
for n being Nat holds (Partial_Sums (- seq)) . n = - ((Partial_Sums seq) . n)
proof end;

theorem Th44: :: MESFUN11:44
for seq being ExtREAL_sequence holds Partial_Sums (- seq) = - (Partial_Sums seq)
proof end;

theorem Th45: :: MESFUN11:45
for seq being ExtREAL_sequence st seq is summable holds
- seq is summable
proof end;

theorem Th46: :: MESFUN11:46
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V121() ) holds
F is additive
proof end;

theorem Th47: :: MESFUN11:47
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is V120() ) holds
F is additive
proof end;

theorem Th48: :: MESFUN11:48
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X st F # x is summable holds
( (- F) # x is summable & Sum ((- F) # x) = - (Sum (F # x)) )
proof end;

theorem Th49: :: MESFUN11:49
for X being non empty set
for S being SigmaField of X
for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom & ( for x being Element of X st x in dom (F . 0) holds
F # x is summable ) holds
lim (Partial_Sums (- F)) = - (lim (Partial_Sums F))
proof end;

theorem Th50: :: MESFUN11:50
for X being non empty set
for S being SigmaField of X
for F, G being Functional_Sequence of X,ExtREAL
for E being Element of S st E c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | E ) holds
lim (Partial_Sums G) = (lim (Partial_Sums F)) | E
proof end;

theorem :: MESFUN11:51
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being nonnegative PartFunc of X,ExtREAL holds integral' (M,(max- (- f))) = integral' (M,f)
proof end;

theorem Th52: :: MESFUN11:52
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))
proof end;

theorem :: MESFUN11:53
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being nonnegative PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable holds
( Integral (M,(max- f)) = 0 & integral+ (M,(max- f)) = 0 )
proof end;

theorem :: MESFUN11:54
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E = dom f & f is E -measurable holds
Integral (M,f) = (Integral (M,(max+ f))) - (Integral (M,(max- f)))
proof end;

theorem Th55: :: MESFUN11:55
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))
proof end;

theorem Th56: :: MESFUN11:56
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive holds
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonpositive ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x >= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) )
proof end;

theorem Th57: :: MESFUN11:57
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) holds
( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )
proof end;

theorem Th58: :: MESFUN11:58
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S holds
( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )
proof end;

Lm3: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive & 0 <= c holds
( Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) & Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) )
proof end;

Lm4: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonnegative & c <= 0 holds
Integral (M,(c (#) f)) = c * (integral' (M,f))
proof end;

theorem Th59: :: MESFUN11:59
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonnegative holds
Integral (M,(c (#) f)) = c * (integral' (M,f))
proof end;

theorem :: MESFUN11:60
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_simple_func_in S & f is nonpositive holds
( Integral (M,(c (#) f)) = (- c) * (integral' (M,(- f))) & Integral (M,(c (#) f)) = - (c * (integral' (M,(- f)))) )
proof end;

theorem Th61: :: MESFUN11:61
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & f is nonpositive holds
0 >= Integral (M,f)
proof end;

theorem :: MESFUN11:62
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proof end;

theorem :: MESFUN11:63
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, E being Element of S st E = dom f & f is E -measurable & f is nonpositive holds
0 >= Integral (M,(f | A))
proof end;

theorem :: MESFUN11:64
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A c= B holds
Integral (M,(f | A)) >= Integral (M,(f | B))
proof end;

theorem :: MESFUN11:65
for X being non empty set
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 E = dom f & f is E -measurable & f is nonpositive & M . (E /\ (eq_dom (f,-infty))) <> 0 holds
Integral (M,f) = -infty
proof end;

theorem :: MESFUN11:66
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is E -measurable & g is E -measurable & f is nonpositive & ( for x being Element of X st x in E holds
g . x <= f . x ) holds
Integral (M,(g | E)) <= Integral (M,(f | E))
proof end;

theorem Th67: :: MESFUN11:67
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for S being SigmaField of X
for E being Element of S
for m being Nat st F is with_the_same_dom & E = dom (F . 0) & ( for n being Nat holds
( F . n is E -measurable & F . n is V121() ) ) holds
(Partial_Sums F) . m is E -measurable
proof end;

theorem :: MESFUN11:68
for X being non empty set
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
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is E -measurable & F . n is nonpositive & I . n = Integral (M,(F . n)) ) ) holds
Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m
proof end;

theorem :: MESFUN11:69
for X being non empty set
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
for f being PartFunc of X,ExtREAL st E c= dom f & f is nonpositive & f is E -measurable & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )
proof end;

theorem :: MESFUN11:70
for X being non empty set
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 E c= dom f & f is nonpositive & f is E -measurable holds
ex F being Functional_Sequence of X,ExtREAL st
( F is additive & ( for n being Nat holds
( F . n is_simple_func_in S & F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
( F # x is summable & f . x = Sum (F # x) ) ) & ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )
proof end;

theorem :: MESFUN11:71
for X being non empty set
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 is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) holds
ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st
for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonpositive ) & ( for j, k being Nat st j <= k holds
for x being Element of X st x in dom (F . n) holds
((FF . n) . j) . x >= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )
proof end;

theorem :: MESFUN11:72
for X being non empty set
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 is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is E -measurable & F . n is nonpositive ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )
proof end;

theorem :: MESFUN11:73
for X being non empty set
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 c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonpositive & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
proof end;

theorem :: MESFUN11:74
for X being non empty set
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 )
proof end;