:: Integral of Measurable Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 24, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC5:1
for x, y being R_eal holds |.(x - y).| = |.(y - x).|
proofend;

theorem Th2: :: MESFUNC5:2
for x, y being R_eal holds y - x <= |.(x - y).|
proofend;

theorem Th3: :: MESFUNC5:3
for x, y being R_eal
for e being real number holds
( not |.(x - y).| < e or ( x = +infty &amp; y = +infty ) or ( x = -infty &amp; y = -infty ) or ( x <> +infty &amp; x <> -infty &amp; y <> +infty &amp; y <> -infty ) )
proofend;

theorem Th4: :: MESFUNC5:4
for n being Nat
for p being R_eal st 0 <= p &amp; p < n holds
ex k being Nat st
( 1 <= k &amp; k <= (2 |^ n) * n &amp; (k - 1) / (2 |^ n) <= p &amp; p < k / (2 |^ n) )
proofend;

theorem Th5: :: MESFUNC5:5
for n, k being Nat
for p being R_eal st k <= (2 |^ n) * n &amp; n <= p holds
k / (2 |^ n) <= p
proofend;

theorem Th6: :: MESFUNC5:6
for x, y, k being ext-real number st 0 <= k holds
( k * (max (x,y)) = max ((k * x),(k * y)) &amp; k * (min (x,y)) = min ((k * x),(k * y)) )
proofend;

theorem :: MESFUNC5:7
for x, y, k being R_eal st k <= 0 holds
( k * (min (x,y)) = max ((k * x),(k * y)) &amp; k * (max (x,y)) = min ((k * x),(k * y)) )
proofend;

begin

definition
let IT be set ;
attrIT is nonpositive  means :Def1: :: MESFUNC5:def 1
 for x being R_eal st x in IT holds
x <= 0 ;
end;

:: deftheorem Def1 defines nonpositive MESFUNC5:def_1_:_
 for IT being set holds
( IT is nonpositive iff for x being R_eal st x in IT holds
x <= 0 );

definition
let R be Relation;
attrR is nonpositive  means :Def2: :: MESFUNC5:def 2
 rng R is nonpositive ;
end;

:: deftheorem Def2 defines nonpositive MESFUNC5:def_2_:_
 for R being Relation holds
( R is nonpositive iff rng R is nonpositive );

theorem Th8: :: MESFUNC5:8
for X being set
for F being PartFunc of X,ExtREAL holds
( F is nonpositive iff for n being set holds F . n <= 0. )
proofend;

theorem Th9: :: MESFUNC5:9
for X being set
for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds
F . n <= 0. ) holds
F is nonpositive
proofend;

definition
let R be Relation;
attrR is without-infty  means :Def3: :: MESFUNC5:def 3
 not -infty in rng R;
attrR is without+infty  means :Def4: :: MESFUNC5:def 4
 not +infty in rng R;
end;

:: deftheorem Def3 defines without-infty MESFUNC5:def_3_:_
 for R being Relation holds
( R is without-infty iff not -infty in rng R );

:: deftheorem Def4 defines without+infty MESFUNC5:def_4_:_
 for R being Relation holds
( R is without+infty iff not +infty in rng R );

definition
let X be non empty set ;
let f be PartFunc of X,ExtREAL;
:: original:without-infty
redefine attrf is without-infty  means :Def5: :: MESFUNC5:def 5
 for x being set holds -infty < f . x;
compatibility
 ( f is without-infty iff for x being set holds -infty < f . x )
proofend;
:: original:without+infty
redefine attrf is without+infty  means :Def6: :: MESFUNC5:def 6
 for x being set holds f . x < +infty ;
compatibility
 ( f is without+infty iff for x being set holds f . x < +infty )
proofend;
end;

:: deftheorem Def5 defines without-infty MESFUNC5:def_5_:_
 for X being non empty set
for f being PartFunc of X,ExtREAL holds
( f is without-infty iff for x being set holds -infty < f . x );

:: deftheorem Def6 defines without+infty MESFUNC5:def_6_:_
 for X being non empty set
for f being PartFunc of X,ExtREAL holds
( f is without+infty iff for x being set holds f . x < +infty );

theorem Th10: :: MESFUNC5:10
for X being non empty set
for f being PartFunc of X,ExtREAL holds
( ( for x being set st x in dom f holds
-infty < f . x ) iff f is () )
proofend;

theorem Th11: :: MESFUNC5:11
for X being non empty set
for f being PartFunc of X,ExtREAL holds
( ( for x being set st x in dom f holds
f . x < +infty ) iff f is () )
proofend;

theorem Th12: :: MESFUNC5:12
for X being non empty set
for f being PartFunc of X,ExtREAL st f is nonnegative holds
f is ()
proofend;

theorem Th13: :: MESFUNC5:13
for X being non empty set
for f being PartFunc of X,ExtREAL st f is nonpositive holds
f is ()
proofend;

registration
let X be non empty set ;
cluster Function-like nonnegative  -> () for Element of bool [:X,ExtREAL:];
coherence
 for b1 being PartFunc of X,ExtREAL st b1 is nonnegative holds
b1 is () by Th12;
cluster Function-like nonpositive  -> () for Element of bool [:X,ExtREAL:];
coherence
 for b1 being PartFunc of X,ExtREAL st b1 is nonpositive holds
b1 is () by Th13;
end;

theorem Th14: :: MESFUNC5:14
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 () &amp; f is () )
proofend;

theorem Th15: :: MESFUNC5:15
for X being non empty set
for Y being set
for f being PartFunc of X,ExtREAL st f is nonnegative holds
f | Y is nonnegative
proofend;

theorem Th16: :: MESFUNC5:16
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is () &amp; g is () holds
dom (f + g) = (dom f) /\ (dom g)
proofend;

theorem :: MESFUNC5:17
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is () &amp; g is () holds
dom (f - g) = (dom f) /\ (dom g)
proofend;

theorem Th18: :: MESFUNC5:18
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for F being Function of RAT,S
for r being Real
for A being Element of S st f is () &amp; g is () &amp; ( for p being Rational holds F . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ) holds
A /\ (less_dom ((f + g),(R_EAL r))) = union (rng F)
proofend;

definition
let X be non empty set ;
let f be PartFunc of X,REAL;
func R_EAL f ->  PartFunc of X,ExtREAL equals :: MESFUNC5:def 7
f;
coherence
 f is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:7;
end;

:: deftheorem  defines R_EAL MESFUNC5:def_7_:_
 for X being non empty set
for f being PartFunc of X,REAL holds R_EAL f = f;

theorem Th19: :: MESFUNC5:19
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 nonnegative &amp; g is nonnegative holds
f + g is nonnegative
proofend;

theorem Th20: :: MESFUNC5:20
for X being non empty set
for f being PartFunc of X,ExtREAL
for c being Real st f is nonnegative holds
( ( 0 <= c implies c (#) f is nonnegative ) &amp; ( c <= 0 implies c (#) f is nonpositive ) )
proofend;

theorem Th21: :: MESFUNC5:21
for X being non empty set
for f, g being PartFunc of X,ExtREAL st ( for x being set st x in (dom f) /\ (dom g) holds
( g . x <= f . x &amp; -infty < g . x &amp; f . x < +infty ) ) holds
f - g is nonnegative
proofend;

Lm1:  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 &amp; max- f is nonnegative &amp; |.f.| is nonnegative )
proofend;

theorem Th22: :: MESFUNC5:22
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is nonnegative &amp; g is nonnegative holds
( dom (f + g) = (dom f) /\ (dom g) &amp; f + g is nonnegative )
proofend;

theorem Th23: :: MESFUNC5:23
for X being non empty set
for f, g, h being PartFunc of X,ExtREAL st f is nonnegative &amp; g is nonnegative &amp; h is nonnegative holds
( dom ((f + g) + h) = ((dom f) /\ (dom g)) /\ (dom h) &amp; (f + g) + h is nonnegative &amp; ( for x being set st x in ((dom f) /\ (dom g)) /\ (dom h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x) ) )
proofend;

theorem Th24: :: MESFUNC5:24
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is () &amp; g is () holds
( dom ((max+ (f + g)) + (max- f)) = (dom f) /\ (dom g) &amp; dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) &amp; dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) &amp; dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) &amp; (max+ (f + g)) + (max- f) is nonnegative &amp; (max- (f + g)) + (max+ f) is nonnegative )
proofend;

theorem Th25: :: MESFUNC5:25
for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is () &amp; f is () &amp; g is () &amp; g is () holds
((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
proofend;

theorem Th26: :: MESFUNC5:26
for C being non empty set
for f being PartFunc of C,ExtREAL
for c being Real st 0 <= c holds
( max+ (c (#) f) = c (#) (max+ f) &amp; max- (c (#) f) = c (#) (max- f) )
proofend;

theorem Th27: :: MESFUNC5:27
for C being non empty set
for f being PartFunc of C,ExtREAL
for c being Real st 0 <= c holds
( max+ ((- c) (#) f) = c (#) (max- f) &amp; max- ((- c) (#) f) = c (#) (max+ f) )
proofend;

theorem Th28: :: MESFUNC5:28
for X being non empty set
for f being PartFunc of X,ExtREAL
for A being set holds
( max+ (f | A) = (max+ f) | A &amp; max- (f | A) = (max- f) | A )
proofend;

theorem Th29: :: MESFUNC5:29
for X being non empty set
for f, g being PartFunc of X,ExtREAL
for B being set st B c= dom (f + g) holds
( dom ((f + g) | B) = B &amp; dom ((f | B) + (g | B)) = B &amp; (f + g) | B = (f | B) + (g | B) )
proofend;

theorem Th30: :: MESFUNC5:30
for X being non empty set
for f being PartFunc of X,ExtREAL
for a being R_eal holds eq_dom (f,a) = f " {a}
proofend;

begin

theorem Th31: :: MESFUNC5:31
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is () &amp; g is () &amp; f is_measurable_on A &amp; g is_measurable_on A holds
f + g is_measurable_on A
proofend;

theorem :: MESFUNC5:32
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 f is_simple_func_in S &amp; dom f = {} holds
ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f &amp; a . 1 = 0 &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0 < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; Sum x = 0 )
proofend;

theorem Th33: :: MESFUNC5:33
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
for r, s being Real st f is_measurable_on A &amp; A c= dom f holds
(A /\ (great_eq_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S
proofend;

theorem Th34: :: MESFUNC5:34
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 f is_simple_func_in S holds
f | A is_simple_func_in S
proofend;

theorem Th35: :: MESFUNC5:35
for X being non empty set
for S being SigmaField of X
for A being Element of S
for F being Finite_Sep_Sequence of S
for G being FinSequence st dom F = dom G &amp; ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) holds
G is Finite_Sep_Sequence of S
proofend;

theorem Th36: :: MESFUNC5:36
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
for F, G being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL st dom F = dom G &amp; ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) &amp; F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
proofend;

theorem Th37: :: MESFUNC5:37
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 f is_simple_func_in S holds
dom f is Element of S
proofend;

Lm2:  for Y being set
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in Y ) holds
p is FinSequence of Y
proofend;

Lm3:  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 &amp; dom f <> {} &amp; g is_simple_func_in S &amp; dom g = dom f holds
( f + g is_simple_func_in S &amp; dom (f + g) <> {} )
proofend;

theorem Th38: :: MESFUNC5:38
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S &amp; g is_simple_func_in S holds
f + g is_simple_func_in S
proofend;

theorem Th39: :: MESFUNC5:39
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 holds
c (#) f is_simple_func_in S
proofend;

theorem Th40: :: MESFUNC5:40
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 &amp; g is_simple_func_in S &amp; ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
f - g is nonnegative
proofend;

theorem Th41: :: MESFUNC5:41
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for c being R_eal st c <> +infty &amp; c <> -infty holds
ex f being PartFunc of X,ExtREAL st
( f is_simple_func_in S &amp; dom f = A &amp; ( for x being set st x in A holds
f . x = c ) )
proofend;

theorem Th42: :: MESFUNC5:42
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 B, BF being Element of S st f is_measurable_on B &amp; BF = (dom f) /\ B holds
f | B is_measurable_on BF
proofend;

theorem Th43: :: MESFUNC5:43
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f, g being PartFunc of X,ExtREAL st A c= dom f &amp; f is_measurable_on A &amp; g is_measurable_on A &amp; f is () &amp; g is () holds
(max+ (f + g)) + (max- f) is_measurable_on A
proofend;

theorem Th44: :: MESFUNC5:44
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f, g being PartFunc of X,ExtREAL st A c= (dom f) /\ (dom g) &amp; f is_measurable_on A &amp; g is_measurable_on A &amp; f is () &amp; g is () holds
(max- (f + g)) + (max+ f) is_measurable_on A
proofend;

theorem Th45: :: MESFUNC5:45
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being set st A in S holds
0 <= M . A
proofend;

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 r being Real st dom f in S &amp; ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
proofend;

theorem Th46: :: MESFUNC5:46
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 ex E1 being Element of S st
( E1 = dom f &amp; f is_measurable_on E1 ) &amp; ex E2 being Element of S st
( E2 = dom g &amp; g is_measurable_on E2 ) &amp; f " {+infty} in S &amp; f " {-infty} in S &amp; g " {+infty} in S &amp; g " {-infty} in S holds
dom (f + g) in S
proofend;

Lm5:  for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,ExtREAL
for r being real number holds A /\ (less_dom (f,(R_EAL r))) = less_dom ((f | A),(R_EAL r))
proofend;

Lm6:  for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for f being PartFunc of X,ExtREAL holds
( f | A is_measurable_on A iff f is_measurable_on A )
proofend;

Lm7:  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 ex E1 being Element of S st
( E1 = dom f &amp; f is_measurable_on E1 ) &amp; ex E2 being Element of S st
( E2 = dom g &amp; g is_measurable_on E2 ) &amp; dom f = dom g holds
ex DFPG being Element of S st
( DFPG = dom (f + g) &amp; f + g is_measurable_on DFPG )
proofend;

theorem Th47: :: MESFUNC5:47
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 ex E1 being Element of S st
( E1 = dom f &amp; f is_measurable_on E1 ) &amp; ex E2 being Element of S st
( E2 = dom g &amp; g is_measurable_on E2 ) holds
ex E being Element of S st
( E = dom (f + g) &amp; f + g is_measurable_on E )
proofend;

theorem Th48: :: MESFUNC5:48
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 being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
proofend;

theorem Th49: :: MESFUNC5:49
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 dom f = A holds
for c being Real
for B being Element of S st f is_measurable_on B holds
c (#) f is_measurable_on B
proofend;

begin

definition
mode ExtREAL_sequence is Function of NAT,ExtREAL;
end;

definition
let seq be ExtREAL_sequence;
attrseq is convergent_to_finite_number  means :Def8: :: MESFUNC5:def 8
 ex g being real number st
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL g)).| < p;
end;

:: deftheorem Def8 defines convergent_to_finite_number MESFUNC5:def_8_:_
 for seq being ExtREAL_sequence holds
( seq is convergent_to_finite_number iff ex g being real number st
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (R_EAL g)).| < p );

definition
let seq be ExtREAL_sequence;
attrseq is convergent_to_+infty  means :Def9: :: MESFUNC5:def 9
 for g being real number st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m;
end;

:: deftheorem Def9 defines convergent_to_+infty MESFUNC5:def_9_:_
 for seq being ExtREAL_sequence holds
( seq is convergent_to_+infty iff for g being real number st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m );

definition
let seq be ExtREAL_sequence;
attrseq is convergent_to_-infty  means :Def10: :: MESFUNC5:def 10
 for g being real number st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g;
end;

:: deftheorem Def10 defines convergent_to_-infty MESFUNC5:def_10_:_
 for seq being ExtREAL_sequence holds
( seq is convergent_to_-infty iff for g being real number st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g );

theorem Th50: :: MESFUNC5:50
for seq being ExtREAL_sequence st seq is convergent_to_+infty holds
( not seq is convergent_to_-infty &amp; not seq is convergent_to_finite_number )
proofend;

theorem Th51: :: MESFUNC5:51
for seq being ExtREAL_sequence st seq is convergent_to_-infty holds
( not seq is convergent_to_+infty &amp; not seq is convergent_to_finite_number )
proofend;

definition
let seq be ExtREAL_sequence;
attrseq is convergent  means :Def11: :: MESFUNC5:def 11
( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty );
end;

:: deftheorem Def11 defines convergent MESFUNC5:def_11_:_
 for seq being ExtREAL_sequence holds
( seq is convergent iff ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) );

definition
let seq be ExtREAL_sequence;
assume A1: seq is convergent ;
func lim seq ->  R_eal means :Def12: :: MESFUNC5:def 12
( ex g being real number st
( it = 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) - it).| < p ) &amp; seq is convergent_to_finite_number ) or ( it = +infty &amp; seq is convergent_to_+infty ) or ( it = -infty &amp; seq is convergent_to_-infty ) );
existence
 ex b1 being R_eal st
( ex g being real number st
( b1 = 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) - b1).| < p ) &amp; seq is convergent_to_finite_number ) or ( b1 = +infty &amp; seq is convergent_to_+infty ) or ( b1 = -infty &amp; seq is convergent_to_-infty ) )
proofend;
uniqueness
 for b1, b2 being R_eal st ( ex g being real number st
( b1 = 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) - b1).| < p ) &amp; seq is convergent_to_finite_number ) or ( b1 = +infty &amp; seq is convergent_to_+infty ) or ( b1 = -infty &amp; seq is convergent_to_-infty ) ) &amp; ( ex g being real number st
( b2 = 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) - b2).| < p ) &amp; seq is convergent_to_finite_number ) or ( b2 = +infty &amp; seq is convergent_to_+infty ) or ( b2 = -infty &amp; seq is convergent_to_-infty ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines lim MESFUNC5:def_12_:_
 for seq being ExtREAL_sequence st seq is convergent holds
for b2 being R_eal holds
( b2 = lim seq iff ( ex g being real number st
( b2 = 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) - b2).| < p ) &amp; seq is convergent_to_finite_number ) or ( b2 = +infty &amp; seq is convergent_to_+infty ) or ( b2 = -infty &amp; seq is convergent_to_-infty ) ) );

theorem Th52: :: MESFUNC5:52
for seq being ExtREAL_sequence
for r being real number st ( for n being Nat holds seq . n = r ) holds
( seq is convergent_to_finite_number &amp; lim seq = r )
proofend;

theorem Th53: :: MESFUNC5:53
for F being FinSequence of ExtREAL st ( for n being Nat st n in dom F holds
0 <= F . n ) holds
0 <= Sum F
proofend;

theorem Th54: :: MESFUNC5:54
for L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds
L . n <= L . m ) holds
( L is convergent &amp; lim L = sup (rng L) )
proofend;

theorem Th55: :: MESFUNC5:55
for L, G being ExtREAL_sequence st ( for n being Nat holds L . n <= G . n ) holds
sup (rng L) <= sup (rng G)
proofend;

theorem Th56: :: MESFUNC5:56
for L being ExtREAL_sequence
for n being Nat holds L . n <= sup (rng L)
proofend;

theorem Th57: :: MESFUNC5:57
for L being ExtREAL_sequence
for K being R_eal st ( for n being Nat holds L . n <= K ) holds
sup (rng L) <= K
proofend;

theorem :: MESFUNC5:58
for L being ExtREAL_sequence
for K being R_eal st K <> +infty &amp; ( for n being Nat holds L . n <= K ) holds
sup (rng L) < +infty
proofend;

theorem Th59: :: MESFUNC5:59
for L being ExtREAL_sequence st L is () holds
( sup (rng L) <> +infty iff ex K being real number st
( 0 < K &amp; ( for n being Nat holds L . n <= K ) ) )
proofend;

theorem Th60: :: MESFUNC5:60
for L being ExtREAL_sequence
for c being ext-real number st ( for n being Nat holds L . n = c ) holds
( L is convergent &amp; lim L = c &amp; lim L = sup (rng L) )
proofend;

Lm8:  for J being ExtREAL_sequence holds
( not J is () or sup (rng J) in REAL or sup (rng J) = +infty )
proofend;

theorem Th61: :: MESFUNC5:61
for J, K, L being ExtREAL_sequence st ( for n, m being Nat st n <= m holds
J . n <= J . m ) &amp; ( for n, m being Nat st n <= m holds
K . n <= K . m ) &amp; J is () &amp; K is () &amp; ( for n being Nat holds (J . n) + (K . n) = L . n ) holds
( L is convergent &amp; lim L = sup (rng L) &amp; lim L = (lim J) + (lim K) &amp; sup (rng L) = (sup (rng K)) + (sup (rng J)) )
proofend;

theorem Th62: :: MESFUNC5:62
for L, K being ExtREAL_sequence
for c being Real st 0 <= c &amp; L is () &amp; ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) holds
( sup (rng K) = (R_EAL c) * (sup (rng L)) &amp; K is () )
proofend;

theorem Th63: :: MESFUNC5:63
for L, K being ExtREAL_sequence
for c being Real st 0 <= c &amp; ( for n, m being Nat st n <= m holds
L . n <= L . m ) &amp; ( for n being Nat holds K . n = (R_EAL c) * (L . n) ) &amp; L is () holds
( ( for n, m being Nat st n <= m holds
K . n <= K . m ) &amp; K is () &amp; K is convergent &amp; lim K = sup (rng K) &amp; lim K = (R_EAL c) * (lim L) )
proofend;

begin

definition
let X be non empty set ;
let H be Functional_Sequence of X,ExtREAL;
let x be Element of X;
funcH # x ->  ExtREAL_sequence means :Def13: :: MESFUNC5:def 13
 for n being Nat holds it . n = (H . n) . x;
existence
 ex b1 being ExtREAL_sequence st
for n being Nat holds b1 . n = (H . n) . x
proofend;
uniqueness
 for b1, b2 being ExtREAL_sequence st ( for n being Nat holds b1 . n = (H . n) . x ) &amp; ( for n being Nat holds b2 . n = (H . n) . x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines # MESFUNC5:def_13_:_
 for X being non empty set
for H being Functional_Sequence of X,ExtREAL
for x being Element of X
for b4 being ExtREAL_sequence holds
( b4 = H # x iff for n being Nat holds b4 . n = (H . n) . x );

definition
let D1, D2 be set ;
let F be Function of NAT,(PFuncs (D1,D2));
let n be Nat;
:: original:.
redefine funcF . n ->  PartFunc of D1,D2;
coherence
 F . n is PartFunc of D1,D2
proofend;
end;

theorem Th64: :: MESFUNC5:64
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 &amp; f is_measurable_on A ) &amp; f is nonnegative holds
ex F being Functional_Sequence of X,ExtREAL st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) )
proofend;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
func integral' (M,f) ->  Element of ExtREAL  equals :Def14: :: MESFUNC5:def 14
 integral (X,S,M,f) if  dom f <> {}
otherwise  0. ;
correctness
coherence
( ( dom f <> {} implies integral (X,S,M,f) is Element of ExtREAL ) &amp; ( not dom f <> {} implies 0. is Element of ExtREAL ) );
consistency
for b1 being Element of ExtREAL holds verum;
;
end;

:: deftheorem Def14 defines integral' MESFUNC5:def_14_:_
 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
( ( dom f <> {} implies integral' (M,f) = integral (X,S,M,f) ) &amp; ( not dom f <> {} implies integral' (M,f) = 0. ) );

theorem Th65: :: MESFUNC5:65
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 &amp; g is_simple_func_in S &amp; f is nonnegative &amp; g is nonnegative holds
( dom (f + g) = (dom f) /\ (dom g) &amp; integral' (M,(f + g)) = (integral' (M,(f | (dom (f + g))))) + (integral' (M,(g | (dom (f + g))))) )
proofend;

theorem Th66: :: MESFUNC5:66
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 &amp; f is nonnegative &amp; 0 <= c holds
integral' (M,(c (#) f)) = (R_EAL c) * (integral' (M,f))
proofend;

theorem Th67: :: MESFUNC5:67
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 being Element of S st f is_simple_func_in S &amp; f is nonnegative &amp; A misses B holds
integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B)))
proofend;

theorem Th68: :: MESFUNC5:68
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 f is_simple_func_in S &amp; f is nonnegative holds
0 <= integral' (M,f)
proofend;

Lm9:  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 &amp; dom f <> {} &amp; f is nonnegative &amp; g is_simple_func_in S &amp; dom g = dom f &amp; g is nonnegative &amp; ( for x being set st x in dom f holds
g . x <= f . x ) holds
( f - g is_simple_func_in S &amp; dom (f - g) <> {} &amp; f - g is nonnegative &amp; integral (X,S,M,f) = (integral (X,S,M,(f - g))) + (integral (X,S,M,g)) )
proofend;

theorem Th69: :: MESFUNC5:69
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 &amp; f is nonnegative &amp; g is_simple_func_in S &amp; g is nonnegative &amp; ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
( dom (f - g) = (dom f) /\ (dom g) &amp; integral' (M,(f | (dom (f - g)))) = (integral' (M,(f - g))) + (integral' (M,(g | (dom (f - g))))) )
proofend;

theorem Th70: :: MESFUNC5:70
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 &amp; g is_simple_func_in S &amp; f is nonnegative &amp; g is nonnegative &amp; ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
integral' (M,(g | (dom (f - g)))) <= integral' (M,(f | (dom (f - g))))
proofend;

theorem Th71: :: MESFUNC5:71
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 R_eal st 0 <= c &amp; f is_simple_func_in S &amp; ( for x being set st x in dom f holds
f . x = c ) holds
integral' (M,f) = c * (M . (dom f))
proofend;

theorem Th72: :: MESFUNC5:72
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 f is_simple_func_in S &amp; f is nonnegative holds
integral' (M,(f | (eq_dom (f,(R_EAL 0))))) = 0
proofend;

theorem Th73: :: MESFUNC5:73
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for B being Element of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S &amp; M . B = 0 &amp; f is nonnegative holds
integral' (M,(f | B)) = 0
proofend;

theorem Th74: :: MESFUNC5:74
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL
for L being ExtREAL_sequence st g is_simple_func_in S &amp; ( for x being set st x in dom g holds
0 < g . x ) &amp; ( for n being Nat holds F . n is_simple_func_in S ) &amp; ( for n being Nat holds dom (F . n) = dom g ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(F . n) . x <= (F . m) . x ) &amp; ( for x being Element of X st x in dom g holds
( F # x is convergent &amp; g . x <= lim (F # x) ) ) &amp; ( for n being Nat holds L . n = integral' (M,(F . n)) ) holds
( L is convergent &amp; integral' (M,g) <= lim L )
proofend;

theorem Th75: :: MESFUNC5:75
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for g being PartFunc of X,ExtREAL
for F being Functional_Sequence of X,ExtREAL st g is_simple_func_in S &amp; g is nonnegative &amp; ( for n being Nat holds F . n is_simple_func_in S ) &amp; ( for n being Nat holds dom (F . n) = dom g ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom g holds
(F . n) . x <= (F . m) . x ) &amp; ( for x being Element of X st x in dom g holds
( F # x is convergent &amp; g . x <= lim (F # x) ) ) holds
ex G being ExtREAL_sequence st
( ( for n being Nat holds G . n = integral' (M,(F . n)) ) &amp; G is convergent &amp; sup (rng G) = lim G &amp; integral' (M,g) <= lim G )
proofend;

theorem Th76: :: MESFUNC5:76
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for F, G being Functional_Sequence of X,ExtREAL
for K, L being ExtREAL_sequence st ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = A ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(F . n) . x <= (F . m) . x ) &amp; ( for n being Nat holds
( G . n is_simple_func_in S &amp; dom (G . n) = A ) ) &amp; ( for n being Nat holds G . n is nonnegative ) &amp; ( for n, m being Nat st n <= m holds
for x being Element of X st x in A holds
(G . n) . x <= (G . m) . x ) &amp; ( for x being Element of X st x in A holds
( F # x is convergent &amp; G # x is convergent &amp; lim (F # x) = lim (G # x) ) ) &amp; ( for n being Nat holds
( K . n = integral' (M,(F . n)) &amp; L . n = integral' (M,(G . n)) ) ) holds
( K is convergent &amp; L is convergent &amp; lim K = lim L )
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
assume that
A1: ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) and
A2: f is nonnegative ;
func integral+ (M,f) ->  Element of ExtREAL  means :Def15: :: MESFUNC5:def 15
 ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) &amp; ( for n being Nat holds K . n = integral' (M,(F . n)) ) &amp; K is convergent &amp; it = lim K );
existence
 ex b1 being Element of ExtREAL ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) &amp; ( for n being Nat holds K . n = integral' (M,(F . n)) ) &amp; K is convergent &amp; b1 = lim K )
proofend;
uniqueness
 for b1, b2 being Element of ExtREAL st ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) &amp; ( for n being Nat holds K . n = integral' (M,(F . n)) ) &amp; K is convergent &amp; b1 = lim K ) &amp; ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) &amp; ( for n being Nat holds K . n = integral' (M,(F . n)) ) &amp; K is convergent &amp; b2 = lim K ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines integral+ MESFUNC5:def_15_:_
 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 &amp; f is_measurable_on A ) &amp; f is nonnegative holds
for b5 being Element of ExtREAL holds
( b5 = integral+ (M,f) iff ex F being Functional_Sequence of X,ExtREAL ex K being ExtREAL_sequence st
( ( for n being Nat holds
( F . n is_simple_func_in S &amp; dom (F . n) = dom f ) ) &amp; ( for n being Nat holds F . n is nonnegative ) &amp; ( 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 ) &amp; ( for x being Element of X st x in dom f holds
( F # x is convergent &amp; lim (F # x) = f . x ) ) &amp; ( for n being Nat holds K . n = integral' (M,(F . n)) ) &amp; K is convergent &amp; b5 = lim K ) );

theorem Th77: :: MESFUNC5:77
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 f is_simple_func_in S &amp; f is nonnegative holds
integral+ (M,f) = integral' (M,f)
proofend;

Lm10:  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 ex A being Element of S st
( A = dom f &amp; A = dom g &amp; f is_measurable_on A &amp; g is_measurable_on A ) &amp; f is nonnegative &amp; g is nonnegative holds
integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))
proofend;

theorem Th78: :: MESFUNC5:78
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 ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) &amp; ex B being Element of S st
( B = dom g &amp; g is_measurable_on B ) &amp; f is nonnegative &amp; g is nonnegative holds
ex C being Element of S st
( C = dom (f + g) &amp; integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
proofend;

theorem Th79: :: MESFUNC5:79
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 &amp; f is_measurable_on A ) &amp; f is nonnegative holds
0 <= integral+ (M,f)
proofend;

theorem Th80: :: MESFUNC5:80
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 ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative holds
0 <= integral+ (M,(f | A))
proofend;

theorem Th81: :: MESFUNC5:81
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 being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative &amp; A misses B holds
integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
proofend;

theorem Th82: :: MESFUNC5:82
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 ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative &amp; M . A = 0 holds
integral+ (M,(f | A)) = 0
proofend;

theorem Th83: :: MESFUNC5:83
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 being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative &amp; A c= B holds
integral+ (M,(f | A)) <= integral+ (M,(f | B))
proofend;

theorem Th84: :: MESFUNC5:84
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, A being Element of S st f is nonnegative &amp; E = dom f &amp; f is_measurable_on E &amp; M . A = 0 holds
integral+ (M,(f | (E \ A))) = integral+ (M,f)
proofend;

theorem Th85: :: MESFUNC5:85
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 ex E being Element of S st
( E = dom f &amp; E = dom g &amp; f is_measurable_on E &amp; g is_measurable_on E ) &amp; f is nonnegative &amp; g is nonnegative &amp; ( for x being Element of X st x in dom g holds
g . x <= f . x ) holds
integral+ (M,g) <= integral+ (M,f)
proofend;

theorem Th86: :: MESFUNC5:86
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 0 <= c &amp; ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) &amp; f is nonnegative holds
integral+ (M,(c (#) f)) = (R_EAL c) * (integral+ (M,f))
proofend;

theorem Th87: :: MESFUNC5:87
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 &amp; f is_measurable_on A ) &amp; ( for x being Element of X st x in dom f holds
0 = f . x ) holds
integral+ (M,f) = 0
proofend;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
func Integral (M,f) ->  Element of ExtREAL  equals :: MESFUNC5:def 16
(integral+ (M,(max+ f))) - (integral+ (M,(max- f)));
coherence
 (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) is Element of ExtREAL ;
end;

:: deftheorem  defines Integral MESFUNC5:def_16_:_
 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 Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f)));

theorem Th88: :: MESFUNC5:88
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 &amp; f is_measurable_on A ) &amp; f is nonnegative holds
Integral (M,f) = integral+ (M,f)
proofend;

theorem :: MESFUNC5:89
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 f is_simple_func_in S &amp; f is nonnegative holds
( Integral (M,f) = integral+ (M,f) &amp; Integral (M,f) = integral' (M,f) )
proofend;

theorem :: MESFUNC5:90
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 &amp; f is_measurable_on A ) &amp; f is nonnegative holds
0 <= Integral (M,f)
proofend;

theorem :: MESFUNC5:91
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 being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative &amp; A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proofend;

theorem :: MESFUNC5:92
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 ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative holds
0 <= Integral (M,(f | A))
proofend;

theorem :: MESFUNC5:93
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 being Element of S st ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; f is nonnegative &amp; A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B))
proofend;

theorem :: MESFUNC5:94
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 ex E being Element of S st
( E = dom f &amp; f is_measurable_on E ) &amp; M . A = 0 holds
Integral (M,(f | A)) = 0
proofend;

theorem Th95: :: MESFUNC5:95
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, A being Element of S st E = dom f &amp; f is_measurable_on E &amp; M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f)
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
predf is_integrable_on M means :Def17: :: MESFUNC5:def 17
( ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) &amp; integral+ (M,(max+ f)) < +infty &amp; integral+ (M,(max- f)) < +infty );
end;

:: deftheorem Def17 defines is_integrable_on MESFUNC5:def_17_:_
 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
( f is_integrable_on M iff ( ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) &amp; integral+ (M,(max+ f)) < +infty &amp; integral+ (M,(max- f)) < +infty ) );

theorem Th96: :: MESFUNC5:96
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 f is_integrable_on M holds
( 0 <= integral+ (M,(max+ f)) &amp; 0 <= integral+ (M,(max- f)) &amp; -infty < Integral (M,f) &amp; Integral (M,f) < +infty )
proofend;

theorem Th97: :: MESFUNC5:97
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 f is_integrable_on M holds
( integral+ (M,(max+ (f | A))) <= integral+ (M,(max+ f)) &amp; integral+ (M,(max- (f | A))) <= integral+ (M,(max- f)) &amp; f | A is_integrable_on M )
proofend;

theorem Th98: :: MESFUNC5:98
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 being Element of S st f is_integrable_on M &amp; A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
proofend;

theorem :: MESFUNC5:99
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 being Element of S st f is_integrable_on M &amp; B = (dom f) \ A holds
( f | A is_integrable_on M &amp; Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
proofend;

theorem Th100: :: MESFUNC5:100
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 &amp; f is_measurable_on A ) holds
( f is_integrable_on M iff |.f.| is_integrable_on M )
proofend;

theorem :: MESFUNC5:101
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 f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,|.f.|)
proofend;

theorem Th102: :: MESFUNC5:102
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 ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) &amp; dom f = dom g &amp; g is_integrable_on M &amp; ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) holds
( f is_integrable_on M &amp; Integral (M,|.f.|) <= Integral (M,g) )
proofend;

theorem Th103: :: MESFUNC5:103
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 r being Real st dom f in S &amp; 0 <= r &amp; dom f <> {} &amp; ( for x being set st x in dom f holds
f . x = r ) holds
integral (X,S,M,f) = r * (M . (dom f))
proofend;

theorem Th104: :: MESFUNC5:104
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 r being Real st dom f in S &amp; 0 <= r &amp; ( for x being set st x in dom f holds
f . x = r ) holds
integral' (M,f) = (R_EAL r) * (M . (dom f))
proofend;

theorem Th105: :: MESFUNC5:105
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 f is_integrable_on M holds
( f " {+infty} in S &amp; f " {-infty} in S &amp; M . (f " {+infty}) = 0 &amp; M . (f " {-infty}) = 0 &amp; (f " {+infty}) \/ (f " {-infty}) in S &amp; M . ((f " {+infty}) \/ (f " {-infty})) = 0 )
proofend;

theorem Th106: :: MESFUNC5:106
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 &amp; g is_integrable_on M &amp; f is nonnegative &amp; g is nonnegative holds
f + g is_integrable_on M
proofend;

theorem Th107: :: MESFUNC5:107
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 &amp; g is_integrable_on M holds
dom (f + g) in S
proofend;

Lm11:  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 ex E0 being Element of S st
( dom (f + g) = E0 &amp; f + g is_measurable_on E0 ) &amp; f is_integrable_on M &amp; g is_integrable_on M holds
f + g is_integrable_on M
proofend;

theorem Th108: :: MESFUNC5:108
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 &amp; g is_integrable_on M holds
f + g is_integrable_on M
proofend;

Lm12:  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 &amp; g is_integrable_on M &amp; dom f = dom g holds
ex E, NFG, NFPG being Element of S st
( E c= dom f &amp; NFG c= dom f &amp; E = (dom f) \ NFG &amp; f | E is V60() &amp; E = dom (f | E) &amp; f | E is_measurable_on E &amp; f | E is_integrable_on M &amp; Integral (M,f) = Integral (M,(f | E)) &amp; E c= dom g &amp; NFG c= dom g &amp; E = (dom g) \ NFG &amp; g | E is V60() &amp; E = dom (g | E) &amp; g | E is_measurable_on E &amp; g | E is_integrable_on M &amp; Integral (M,g) = Integral (M,(g | E)) &amp; E c= dom (f + g) &amp; NFPG c= dom (f + g) &amp; E = (dom (f + g)) \ NFPG &amp; M . NFG = 0 &amp; M . NFPG = 0 &amp; E = dom ((f + g) | E) &amp; (f + g) | E is_measurable_on E &amp; (f + g) | E is_integrable_on M &amp; (f + g) | E = (f | E) + (g | E) &amp; Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proofend;

Lm13:  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 &amp; g is_integrable_on M &amp; dom f = dom g holds
( f + g is_integrable_on M &amp; Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )
proofend;

theorem :: MESFUNC5:109
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 &amp; g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) &amp; Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proofend;

theorem Th110: :: MESFUNC5:110
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_integrable_on M holds
( c (#) f is_integrable_on M &amp; Integral (M,(c (#) f)) = (R_EAL c) * (Integral (M,f)) )
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,ExtREAL;
let B be Element of S;
func Integral_on (M,B,f) ->  Element of ExtREAL  equals :: MESFUNC5:def 18
 Integral (M,(f | B));
coherence
 Integral (M,(f | B)) is Element of ExtREAL ;
end;

:: deftheorem  defines Integral_on MESFUNC5:def_18_:_
 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 B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

theorem :: MESFUNC5:111
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
for B being Element of S st f is_integrable_on M &amp; g is_integrable_on M &amp; B c= dom (f + g) holds
( f + g is_integrable_on M &amp; Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
proofend;

theorem :: MESFUNC5:112
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
for B being Element of S st f is_integrable_on M holds
( f | B is_integrable_on M &amp; Integral_on (M,B,(c (#) f)) = (R_EAL c) * (Integral_on (M,B,f)) )
proofend;