:: The Lebesgue Monotone Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC9:1
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V120() holds
dom (f + g) = (dom f) /\ (dom g)
proofend;

theorem Th2: :: MESFUNC9:2
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V119() holds
dom (f - g) = (dom f) /\ (dom g)
proofend;

theorem Th3: :: MESFUNC9:3
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V119() & g is V119() holds
f + g is V119()
proofend;

theorem Th4: :: MESFUNC9:4
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V120() holds
f + g is V120()
proofend;

theorem :: MESFUNC9:5
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V119() & g is V120() holds
f - g is V119()
proofend;

theorem :: MESFUNC9:6
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is V120() & g is V119() holds
f - g is V120()
proofend;

theorem Th7: :: MESFUNC9:7
for seq being ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies ex g being real number st
( lim seq = g &amp; ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim seq)).| < p ) ) ) &amp; ( seq is convergent_to_+infty implies lim seq = +infty ) &amp; ( seq is convergent_to_-infty implies lim seq = -infty ) )
proofend;

theorem Th8: :: MESFUNC9:8
for seq being ExtREAL_sequence st seq is V111() holds
not seq is convergent_to_-infty
proofend;

theorem Th9: :: MESFUNC9:9
for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent &amp; ( for k being Nat holds seq . k <= p ) holds
lim seq <= p
proofend;

theorem Th10: :: MESFUNC9:10
for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent &amp; ( for k being Nat holds p <= seq . k ) holds
p <= lim seq
proofend;

theorem Th11: :: MESFUNC9:11
for seq1, seq2, seq being ExtREAL_sequence st seq1 is convergent &amp; seq2 is convergent &amp; seq1 is V111() &amp; seq2 is V111() &amp; ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) holds
( seq is V111() &amp; seq is convergent &amp; lim seq = (lim seq1) + (lim seq2) )
proofend;

theorem Th12: :: MESFUNC9:12
for X being non empty set
for G, F being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st ( for n being Nat holds G . n = (F . n) | D ) &amp; x in D holds
( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) &amp; ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) &amp; ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) &amp; ( F # x is convergent implies G # x is convergent ) )
proofend;

theorem Th13: :: MESFUNC9:13
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 &amp; f is_measurable_on E &amp; f is nonnegative &amp; M . (E /\ (eq_dom (f,+infty))) <> 0 holds
Integral (M,f) = +infty
proofend;

theorem :: MESFUNC9:14
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 holds
( Integral (M,(chi (E,X))) = M . E &amp; Integral (M,((chi (E,X)) | E)) = M . E )
proofend;

theorem Th15: :: MESFUNC9:15
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 &amp; E c= dom g &amp; f is_measurable_on E &amp; g is_measurable_on E &amp; f is nonnegative &amp; ( for x being Element of X st x in E holds
f . x <= g . x ) holds
Integral (M,(f | E)) <= Integral (M,(g | E))
proofend;

begin

definition
let f be ext-real-valued Function;
let x be set ;
:: original:.
redefine funcf . x ->  Element of ExtREAL ;
coherence
 f . x is Element of ExtREAL by XXREAL_0:def_1;
end;

definition
let s be ext-real-valued Function;
func Partial_Sums s ->  ExtREAL_sequence means :Def1: :: MESFUNC9:def 1
( it . 0 = s . 0 &amp; ( for n being Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );
existence
 ex b1 being ExtREAL_sequence st
( b1 . 0 = s . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being ExtREAL_sequence st b1 . 0 = s . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) &amp; b2 . 0 = s . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines Partial_Sums MESFUNC9:def_1_:_
 for s being ext-real-valued Function
for b2 being ExtREAL_sequence holds
( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) );

definition
let s be ext-real-valued Function;
attrs is summable  means :Def2: :: MESFUNC9:def 2
 Partial_Sums s is convergent ;
end;

:: deftheorem Def2 defines summable MESFUNC9:def_2_:_
 for s being ext-real-valued Function holds
( s is summable iff Partial_Sums s is convergent );

definition
let s be ext-real-valued Function;
func Sum s ->  R_eal equals :: MESFUNC9:def 3
 lim (Partial_Sums s);
correctness
coherence
lim (Partial_Sums s) is R_eal;
;
end;

:: deftheorem  defines Sum MESFUNC9:def_3_:_
 for s being ext-real-valued Function holds Sum s = lim (Partial_Sums s);

theorem Th16: :: MESFUNC9:16
for seq being ExtREAL_sequence st seq is V111() holds
( Partial_Sums seq is V111() &amp; Partial_Sums seq is non-decreasing )
proofend;

theorem :: MESFUNC9:17
for seq being ExtREAL_sequence st ( for n being Nat holds 0 < seq . n ) holds
for m being Nat holds 0 < (Partial_Sums seq) . m
proofend;

theorem Th18: :: MESFUNC9:18
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is with_the_same_dom &amp; ( for n being Nat holds G . n = (F . n) | D ) holds
G is with_the_same_dom
proofend;

theorem Th19: :: MESFUNC9:19
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st D c= dom (F . 0) &amp; ( for n being Nat holds G . n = (F . n) | D ) &amp; ( for x being Element of X st x in D holds
F # x is convergent ) holds
(lim F) | D = lim G
proofend;

theorem Th20: :: MESFUNC9:20
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL
for n being Nat st F is with_the_same_dom &amp; E c= dom (F . 0) &amp; ( for m being Nat holds
( F . m is_measurable_on E &amp; G . m = (F . m) | E ) ) holds
G . n is_measurable_on E
proofend;

theorem Th21: :: MESFUNC9:21
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) &amp; G is with_the_same_dom &amp; ( for x being Element of X st x in E holds
F # x is summable ) &amp; ( for n being Nat holds G . n = (F . n) | E ) holds
for x being Element of X st x in E holds
G # x is summable
proofend;

begin

definition
let X be non empty set ;
let F be Functional_Sequence of X,ExtREAL;
func Partial_Sums F ->  Functional_Sequence of X,ExtREAL means :Def4: :: MESFUNC9:def 4
( it . 0 = F . 0 &amp; ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );
existence
 ex b1 being Functional_Sequence of X,ExtREAL st
( b1 . 0 = F . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) )
proofend;
uniqueness
 for b1, b2 being Functional_Sequence of X,ExtREAL st b1 . 0 = F . 0 &amp; ( for n being Nat holds b1 . (n + 1) = (b1 . n) + (F . (n + 1)) ) &amp; b2 . 0 = F . 0 &amp; ( for n being Nat holds b2 . (n + 1) = (b2 . n) + (F . (n + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines Partial_Sums MESFUNC9:def_4_:_
 for X being non empty set
for F, b3 being Functional_Sequence of X,ExtREAL holds
( b3 = Partial_Sums F iff ( b3 . 0 = F . 0 &amp; ( for n being Nat holds b3 . (n + 1) = (b3 . n) + (F . (n + 1)) ) ) );

definition
let X be set ;
let F be Functional_Sequence of X,ExtREAL;
attrF is additive  means :Def5: :: MESFUNC9:def 5
 for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty );
end;

:: deftheorem Def5 defines additive MESFUNC9:def_5_:_
 for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is additive iff for n, m being Nat st n <> m holds
for x being set holds
( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) );

Lm1:  for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) &amp; m <= n holds
z in dom ((Partial_Sums F) . m)
proofend;

theorem Th22: :: MESFUNC9:22
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st z in dom ((Partial_Sums F) . n) &amp; m <= n holds
( z in dom ((Partial_Sums F) . m) &amp; z in dom (F . m) )
proofend;

theorem Th23: :: MESFUNC9:23
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) &amp; ((Partial_Sums F) . n) . z = +infty holds
ex m being Nat st
( m <= n &amp; (F . m) . z = +infty )
proofend;

theorem :: MESFUNC9:24
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st F is additive &amp; z in dom ((Partial_Sums F) . n) &amp; ((Partial_Sums F) . n) . z = +infty &amp; m <= n holds
(F . m) . z <> -infty
proofend;

theorem Th25: :: MESFUNC9:25
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for z being set st z in dom ((Partial_Sums F) . n) &amp; ((Partial_Sums F) . n) . z = -infty holds
ex m being Nat st
( m <= n &amp; (F . m) . z = -infty )
proofend;

theorem :: MESFUNC9:26
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for z being set st F is additive &amp; z in dom ((Partial_Sums F) . n) &amp; ((Partial_Sums F) . n) . z = -infty &amp; m <= n holds
(F . m) . z <> +infty
proofend;

theorem Th27: :: MESFUNC9:27
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} &amp; (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )
proofend;

theorem Th28: :: MESFUNC9:28
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive holds
dom ((Partial_Sums F) . n) = meet  {  (dom (F . k)) where k is Element of NAT : k <= n  }
proofend;

theorem Th29: :: MESFUNC9:29
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st F is additive &amp; F is with_the_same_dom holds
dom ((Partial_Sums F) . n) = dom (F . 0)
proofend;

theorem Th30: :: MESFUNC9:30
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds
F is additive
proofend;

theorem Th31: :: MESFUNC9:31
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for D being set st F is additive &amp; ( for n being Nat holds G . n = (F . n) | D ) holds
G is additive
proofend;

theorem Th32: :: MESFUNC9:32
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat
for x being Element of X
for D being set st F is additive &amp; F is with_the_same_dom &amp; D c= dom (F . 0) &amp; x in D holds
(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n
proofend;

theorem Th33: :: MESFUNC9:33
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X
for D being set st F is additive &amp; F is with_the_same_dom &amp; D c= dom (F . 0) &amp; x in D holds
( ( Partial_Sums (F # x) is convergent_to_finite_number implies (Partial_Sums F) # x is convergent_to_finite_number ) &amp; ( (Partial_Sums F) # x is convergent_to_finite_number implies Partial_Sums (F # x) is convergent_to_finite_number ) &amp; ( Partial_Sums (F # x) is convergent_to_+infty implies (Partial_Sums F) # x is convergent_to_+infty ) &amp; ( (Partial_Sums F) # x is convergent_to_+infty implies Partial_Sums (F # x) is convergent_to_+infty ) &amp; ( Partial_Sums (F # x) is convergent_to_-infty implies (Partial_Sums F) # x is convergent_to_-infty ) &amp; ( (Partial_Sums F) # x is convergent_to_-infty implies Partial_Sums (F # x) is convergent_to_-infty ) &amp; ( Partial_Sums (F # x) is convergent implies (Partial_Sums F) # x is convergent ) &amp; ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent ) )
proofend;

theorem Th34: :: MESFUNC9:34
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL
for x being Element of X st F is additive &amp; F is with_the_same_dom &amp; dom f c= dom (F . 0) &amp; x in dom f &amp; F # x is summable &amp; f . x = Sum (F # x) holds
f . x = lim ((Partial_Sums F) # x)
proofend;

theorem Th35: :: MESFUNC9:35
for X being non empty set
for S being SigmaField of X
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds
( F is additive &amp; (Partial_Sums F) . n is_simple_func_in S )
proofend;

theorem Th36: :: MESFUNC9:36
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is nonnegative ) holds
(Partial_Sums F) . n is nonnegative
proofend;

theorem Th37: :: MESFUNC9:37
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n, m being Nat
for x being Element of X st F is with_the_same_dom &amp; x in dom (F . 0) &amp; ( for k being Nat holds F . k is nonnegative ) &amp; n <= m holds
((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x
proofend;

theorem Th38: :: MESFUNC9:38
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for x being Element of X st F is with_the_same_dom &amp; x in dom (F . 0) &amp; ( for m being Nat holds F . m is nonnegative ) holds
( (Partial_Sums F) # x is non-decreasing &amp; (Partial_Sums F) # x is convergent )
proofend;

theorem Th39: :: MESFUNC9:39
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is V119() ) holds
(Partial_Sums F) . n is V119()
proofend;

theorem :: MESFUNC9:40
for X being non empty set
for F being Functional_Sequence of X,ExtREAL
for n being Nat st ( for m being Nat holds F . m is V120() ) holds
(Partial_Sums F) . n is V120()
proofend;

theorem Th41: :: MESFUNC9:41
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for m being Nat st ( for n being Nat holds
( F . n is_measurable_on E &amp; F . n is V119() ) ) holds
(Partial_Sums F) . m is_measurable_on E
proofend;

theorem Th42: :: MESFUNC9:42
for X being non empty set
for F, G being Functional_Sequence of X,ExtREAL
for n being Nat
for x being Element of X st F is additive &amp; F is with_the_same_dom &amp; G is additive &amp; G is with_the_same_dom &amp; x in (dom (F . 0)) /\ (dom (G . 0)) &amp; ( for k being Nat
for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds
(F . k) . y <= (G . k) . y ) holds
((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x
proofend;

theorem Th43: :: MESFUNC9:43
for X being non empty set
for F being Functional_Sequence of X,ExtREAL st F is additive &amp; F is with_the_same_dom holds
Partial_Sums F is with_the_same_dom
proofend;

theorem Th44: :: MESFUNC9:44
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st dom (F . 0) = E &amp; F is additive &amp; F is with_the_same_dom &amp; ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) &amp; ( for x being Element of X st x in E holds
F # x is summable ) holds
lim (Partial_Sums F) is_measurable_on E
proofend;

theorem :: MESFUNC9:45
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 st ( for n being Nat holds F . n is_integrable_on M ) holds
for m being Nat holds (Partial_Sums F) . m is_integrable_on M
proofend;

theorem Th46: :: MESFUNC9:46
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 Functional_Sequence of X,ExtREAL
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0) &amp; F is additive &amp; F is with_the_same_dom &amp; ( for n being Nat holds
( F . n is_measurable_on E &amp; F . n is nonnegative &amp; I . n = Integral (M,(F . n)) ) ) holds
Integral (M,((Partial_Sums F) . m)) = (Partial_Sums I) . m
proofend;

begin

Lm2:  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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f &amp; f is_measurable_on E &amp; E = {} &amp; ( for n being Nat holds F . n is_simple_func_in S ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) &amp; I is summable &amp; Integral (M,(f | E)) = Sum I )
proofend;

Lm3:  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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f &amp; f is nonnegative &amp; f is_measurable_on E &amp; F is additive &amp; E common_on_dom F &amp; ( for n being Nat holds
( F . n is_simple_func_in S &amp; F . n is nonnegative ) ) &amp; ( for x being Element of X st x in E holds
( F # x is summable &amp; f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) &amp; I is summable &amp; Integral (M,(f | E)) = Sum I )
proofend;

theorem :: MESFUNC9:47
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 Functional_Sequence of X,ExtREAL
for f being PartFunc of X,ExtREAL st E c= dom f &amp; f is nonnegative &amp; f is_measurable_on E &amp; F is additive &amp; ( for n being Nat holds
( F . n is_simple_func_in S &amp; F . n is nonnegative &amp; E c= dom (F . n) ) ) &amp; ( for x being Element of X st x in E holds
( F # x is summable &amp; f . x = Sum (F # x) ) ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) &amp; I is summable &amp; Integral (M,(f | E)) = Sum I )
proofend;

theorem :: MESFUNC9:48
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 &amp; f is nonnegative &amp; f is_measurable_on E holds
ex g being Functional_Sequence of X,ExtREAL st
( g is additive &amp; ( for n being Nat holds
( g . n is_simple_func_in S &amp; g . n is nonnegative &amp; g . n is_measurable_on E ) ) &amp; ( for x being Element of X st x in E holds
( g # x is summable &amp; f . x = Sum (g # x) ) ) &amp; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) &amp; I is summable &amp; Integral (M,(f | E)) = Sum I ) )
proofend;

registration
let X be non empty set ;
cluster non empty Relation-like NAT -defined PFuncs (X,ExtREAL) -valued Function-like total quasi_total with_the_same_dom additive for Element of bool [:NAT,(PFuncs (X,ExtREAL)):];
existence
 ex b1 being Functional_Sequence of X,ExtREAL st
( b1 is additive &amp; b1 is with_the_same_dom )
proofend;
end;

definition
let C, D, X be non empty set ;
let F be Function of [:C,D:],(PFuncs (X,ExtREAL));
let c be Element of C;
let d be Element of D;
:: original:.
redefine funcF . (c,d) ->  PartFunc of X,ExtREAL;
correctness
coherence
F . (c,d) is PartFunc of X,ExtREAL;
proofend;
end;

definition
let C, D, X be non empty set ;
let F be Function of [:C,D:],X;
let c be Element of C;
func ProjMap1 (F,c) ->  Function of D,X means :: MESFUNC9:def 6
 for d being Element of D holds it . d = F . (c,d);
existence
 ex b1 being Function of D,X st
for d being Element of D holds b1 . d = F . (c,d)
proofend;
uniqueness
 for b1, b2 being Function of D,X st ( for d being Element of D holds b1 . d = F . (c,d) ) &amp; ( for d being Element of D holds b2 . d = F . (c,d) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines ProjMap1 MESFUNC9:def_6_:_
 for C, D, X being non empty set
for F being Function of [:C,D:],X
for c being Element of C
for b6 being Function of D,X holds
( b6 = ProjMap1 (F,c) iff for d being Element of D holds b6 . d = F . (c,d) );

definition
let C, D, X be non empty set ;
let F be Function of [:C,D:],X;
let d be Element of D;
func ProjMap2 (F,d) ->  Function of C,X means :: MESFUNC9:def 7
 for c being Element of C holds it . c = F . (c,d);
existence
 ex b1 being Function of C,X st
for c being Element of C holds b1 . c = F . (c,d)
proofend;
uniqueness
 for b1, b2 being Function of C,X st ( for c being Element of C holds b1 . c = F . (c,d) ) &amp; ( for c being Element of C holds b2 . c = F . (c,d) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines ProjMap2 MESFUNC9:def_7_:_
 for C, D, X being non empty set
for F being Function of [:C,D:],X
for d being Element of D
for b6 being Function of C,X holds
( b6 = ProjMap2 (F,d) iff for c being Element of C holds b6 . c = F . (c,d) );

definition
let X, Y be set ;
let F be Function of [:NAT,NAT:],(PFuncs (X,Y));
let n be Nat;
func ProjMap1 (F,n) ->  Functional_Sequence of X,Y means :Def8: :: MESFUNC9:def 8
 for m being Nat holds it . m = F . (n,m);
existence
 ex b1 being Functional_Sequence of X,Y st
for m being Nat holds b1 . m = F . (n,m)
proofend;
uniqueness
 for b1, b2 being Functional_Sequence of X,Y st ( for m being Nat holds b1 . m = F . (n,m) ) &amp; ( for m being Nat holds b2 . m = F . (n,m) ) holds
b1 = b2
proofend;
func ProjMap2 (F,n) ->  Functional_Sequence of X,Y means :Def9: :: MESFUNC9:def 9
 for m being Nat holds it . m = F . (m,n);
existence
 ex b1 being Functional_Sequence of X,Y st
for m being Nat holds b1 . m = F . (m,n)
proofend;
uniqueness
 for b1, b2 being Functional_Sequence of X,Y st ( for m being Nat holds b1 . m = F . (m,n) ) &amp; ( for m being Nat holds b2 . m = F . (m,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines ProjMap1 MESFUNC9:def_8_:_
 for X, Y being set
for F being Function of [:NAT,NAT:],(PFuncs (X,Y))
for n being Nat
for b5 being Functional_Sequence of X,Y holds
( b5 = ProjMap1 (F,n) iff for m being Nat holds b5 . m = F . (n,m) );

:: deftheorem Def9 defines ProjMap2 MESFUNC9:def_9_:_
 for X, Y being set
for F being Function of [:NAT,NAT:],(PFuncs (X,Y))
for n being Nat
for b5 being Functional_Sequence of X,Y holds
( b5 = ProjMap2 (F,n) iff for m being Nat holds b5 . m = F . (m,n) );

definition
let X be non empty set ;
let F be Function of NAT,(Funcs (NAT,(PFuncs (X,ExtREAL))));
let n be Nat;
:: original:.
redefine funcF . n ->  Functional_Sequence of X,ExtREAL;
correctness
coherence
F . n is Functional_Sequence of X,ExtREAL;
proofend;
end;

theorem Th49: :: MESFUNC9:49
for X being non empty set
for S being SigmaField of X
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) &amp; F is with_the_same_dom &amp; ( for n being Nat holds
( F . n is nonnegative &amp; F . n is_measurable_on E ) ) holds
ex FF being Function of NAT,(Funcs (NAT,(PFuncs (X,ExtREAL)))) st
for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S &amp; dom ((FF . n) . m) = dom (F . n) ) ) &amp; ( for m being Nat holds (FF . n) . m is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent &amp; lim ((FF . n) # x) = (F . n) . x ) ) )
proofend;

theorem Th50: :: MESFUNC9:50
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 Functional_Sequence of X,ExtREAL st E = dom (F . 0) &amp; F is additive &amp; F is with_the_same_dom &amp; ( for n being Nat holds
( F . n is_measurable_on E &amp; F . n is nonnegative ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral (M,(F . n)) &amp; Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )
proofend;

Lm4:  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 Functional_Sequence of X,ExtREAL st E = dom (F . 0) &amp; F is additive &amp; F is with_the_same_dom &amp; ( for n being Nat holds
( F . n is nonnegative &amp; F . n is_measurable_on E ) ) &amp; ( 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)) ) &amp; I is summable &amp; Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
proofend;

theorem Th51: :: MESFUNC9:51
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 Functional_Sequence of X,ExtREAL st E c= dom (F . 0) &amp; F is additive &amp; F is with_the_same_dom &amp; ( for n being Nat holds
( F . n is nonnegative &amp; F . n is_measurable_on E ) ) &amp; ( 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)) ) &amp; I is summable &amp; Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
proofend;

:: Lebesgue Monotone Convergence Theorem
:: [WP: ] Lebesgue's_Monotone_Convergence_Theorem
theorem :: MESFUNC9:52
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 Functional_Sequence of X,ExtREAL st E = dom (F . 0) &amp; F . 0 is nonnegative &amp; F is with_the_same_dom &amp; ( for n being Nat holds F . n is_measurable_on E ) &amp; ( 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 ) &amp; ( 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)) ) &amp; I is convergent &amp; Integral (M,(lim F)) = lim I )
proofend;