:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC6:1
for X being non empty set
for f being PartFunc of X,REAL holds |.(R_EAL f).| = R_EAL (abs f)
proofend;

theorem Th2: :: MESFUNC6:2
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 & ( for x being set st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
proofend;

theorem :: MESFUNC6:3
for X being non empty set
for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x &amp; y < a ) ) )
proofend;

theorem :: MESFUNC6:4
for X being non empty set
for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_eq_dom (f,a) iff ( x in dom f &amp; ex y being Real st
( y = f . x &amp; y <= a ) ) )
proofend;

theorem :: MESFUNC6:5
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_dom (f,r) iff ( x in dom f &amp; ex y being Real st
( y = f . x &amp; r < y ) ) )
proofend;

theorem :: MESFUNC6:6
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in great_eq_dom (f,r) iff ( x in dom f &amp; ex y being Real st
( y = f . x &amp; r <= y ) ) )
proofend;

theorem :: MESFUNC6:7
for X being non empty set
for f being PartFunc of X,REAL
for r being Real
for x being set holds
( x in eq_dom (f,r) iff ( x in dom f &amp; ex y being Real st
( y = f . x &amp; r = y ) ) )
proofend;

theorem :: MESFUNC6:8
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (great_eq_dom (f,r)) = meet (rng F)
proofend;

theorem :: MESFUNC6:9
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (less_eq_dom (f,r)) = meet (rng F)
proofend;

theorem :: MESFUNC6:10
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (less_eq_dom (f,(r - (1 / (n + 1))))) ) holds
Y /\ (less_dom (f,r)) = union (rng F)
proofend;

theorem :: MESFUNC6:11
for X being non empty set
for Y being set
for S being SigmaField of X
for F being Function of NAT,S
for f being PartFunc of X,REAL
for r being Real st ( for n being Nat holds F . n = Y /\ (great_eq_dom (f,(r + (1 / (n + 1))))) ) holds
Y /\ (great_dom (f,r)) = union (rng F)
proofend;

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
let A be Element of S;
predf is_measurable_on A means :Def1: :: MESFUNC6:def 1
 R_EAL f is_measurable_on A;
end;

:: deftheorem Def1 defines is_measurable_on MESFUNC6:def_1_:_
 for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff R_EAL f is_measurable_on A );

theorem Th12: :: MESFUNC6:12
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,r)) in S )
proofend;

theorem Th13: :: MESFUNC6:13
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,r)) in S )
proofend;

theorem :: MESFUNC6:14
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S holds
( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,r)) in S )
proofend;

theorem :: MESFUNC6:15
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st A c= dom f holds
( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,r)) in S )
proofend;

theorem :: MESFUNC6:16
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st B c= A &amp; f is_measurable_on A holds
f is_measurable_on B
proofend;

theorem :: MESFUNC6:17
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A, B being Element of S st f is_measurable_on A &amp; f is_measurable_on B holds
f is_measurable_on A \/ B
proofend;

theorem :: MESFUNC6:18
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
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_dom (f,r))) /\ (less_dom (f,s)) in S
proofend;

theorem :: MESFUNC6:19
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A &amp; g is_measurable_on A &amp; A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S
proofend;

theorem Th20: :: MESFUNC6:20
for X being non empty set
for f being PartFunc of X,REAL
for r being Real holds R_EAL (r (#) f) = r (#) (R_EAL f)
proofend;

theorem Th21: :: MESFUNC6:21
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A &amp; A c= dom f holds
r (#) f is_measurable_on A
proofend;

begin

theorem :: MESFUNC6:22
for X being non empty set
for f being PartFunc of X,REAL holds R_EAL f is V68() ;

theorem Th23: :: MESFUNC6:23
for X being non empty set
for f, g being PartFunc of X,REAL holds
( R_EAL (f + g) = (R_EAL f) + (R_EAL g) &amp; R_EAL (f - g) = (R_EAL f) - (R_EAL g) &amp; dom (R_EAL (f + g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) &amp; dom (R_EAL (f - g)) = (dom (R_EAL f)) /\ (dom (R_EAL g)) &amp; dom (R_EAL (f + g)) = (dom f) /\ (dom g) &amp; dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
proofend;

theorem :: MESFUNC6:24
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real
for F being Function of RAT,S st ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)
proofend;

theorem :: MESFUNC6:25
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A &amp; g is_measurable_on A holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
proofend;

theorem Th26: :: MESFUNC6:26
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A &amp; g is_measurable_on A holds
f + g is_measurable_on A
proofend;

theorem :: MESFUNC6:27
for X being non empty set
for f, g being PartFunc of X,REAL holds (R_EAL f) - (R_EAL g) = (R_EAL f) + (R_EAL (- g))
proofend;

theorem Th28: :: MESFUNC6:28
for X being non empty set
for f being PartFunc of X,REAL holds
( - (R_EAL f) = R_EAL ((- 1) (#) f) &amp; - (R_EAL f) = R_EAL (- f) )
proofend;

theorem :: MESFUNC6:29
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A &amp; g is_measurable_on A &amp; A c= dom g holds
f - g is_measurable_on A
proofend;

begin

theorem Th30: :: MESFUNC6:30
for X being non empty set
for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = max+ f &amp; max- (R_EAL f) = max- f )
proofend;

theorem :: MESFUNC6:31
for X being non empty set
for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max+ f) . x
proofend;

theorem :: MESFUNC6:32
for X being non empty set
for f being PartFunc of X,REAL
for x being Element of X holds 0 <= (max- f) . x
proofend;

theorem :: MESFUNC6:33
for X being non empty set
for f being PartFunc of X,REAL holds max- f = max+ (- f)
proofend;

theorem :: MESFUNC6:34
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; 0 < (max+ f) . x holds
(max- f) . x = 0
proofend;

theorem :: MESFUNC6:35
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; 0 < (max- f) . x holds
(max+ f) . x = 0
proofend;

theorem :: MESFUNC6:36
for X being non empty set
for f being PartFunc of X,REAL holds
( dom f = dom ((max+ f) - (max- f)) &amp; dom f = dom ((max+ f) + (max- f)) )
proofend;

theorem :: MESFUNC6:37
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0 ) &amp; ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
proofend;

theorem :: MESFUNC6:38
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; (max+ f) . x = f . x holds
(max- f) . x = 0
proofend;

theorem :: MESFUNC6:39
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; (max+ f) . x = 0 holds
(max- f) . x = - (f . x)
proofend;

theorem :: MESFUNC6:40
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; (max- f) . x = - (f . x) holds
(max+ f) . x = 0
proofend;

theorem :: MESFUNC6:41
for X being non empty set
for f being PartFunc of X,REAL
for x being set st x in dom f &amp; (max- f) . x = 0 holds
(max+ f) . x = f . x
proofend;

theorem :: MESFUNC6:42
for X being non empty set
for f being PartFunc of X,REAL holds f = (max+ f) - (max- f)
proofend;

theorem Th43: :: MESFUNC6:43
for r being Real holds |.r.| = |.(R_EAL r).|
proofend;

theorem Th44: :: MESFUNC6:44
for X being non empty set
for f being PartFunc of X,REAL holds R_EAL (abs f) = |.(R_EAL f).|
proofend;

theorem :: MESFUNC6:45
for X being non empty set
for f being PartFunc of X,REAL holds abs f = (max+ f) + (max- f)
proofend;

begin

theorem Th46: :: MESFUNC6:46
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A holds
max+ f is_measurable_on A
proofend;

theorem Th47: :: MESFUNC6:47
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A &amp; A c= dom f holds
max- f is_measurable_on A
proofend;

theorem :: MESFUNC6:48
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_measurable_on A &amp; A c= dom f holds
abs f is_measurable_on A
proofend;

begin

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
predf is_simple_func_in S means :Def2: :: MESFUNC6:def 2
 ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) &amp; ( for n being Nat
for x, y being Element of X st n in dom F &amp; x in F . n &amp; y in F . n holds
f . x = f . y ) );
end;

:: deftheorem Def2 defines is_simple_func_in MESFUNC6:def_2_:_
 for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st
( dom f = union (rng F) &amp; ( for n being Nat
for x, y being Element of X st n in dom F &amp; x in F . n &amp; y in F . n holds
f . x = f . y ) ) );

theorem Th49: :: MESFUNC6:49
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S )
proofend;

theorem :: MESFUNC6:50
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A
proofend;

theorem Th51: :: MESFUNC6:51
for X being set
for f being PartFunc of X,REAL holds
( f is nonnegative iff for x being set holds 0 <= f . x )
proofend;

theorem Th52: :: MESFUNC6:52
for X being set
for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
0 <= f . x ) holds
f is nonnegative
proofend;

theorem :: MESFUNC6:53
for X being set
for f being PartFunc of X,REAL holds
( f is nonpositive iff for x being set holds f . x <= 0 )
proofend;

theorem Th54: :: MESFUNC6:54
for X being non empty set
for f being PartFunc of X,REAL st ( for x being set st x in dom f holds
f . x <= 0 ) holds
f is nonpositive
proofend;

theorem :: MESFUNC6:55
for X being non empty set
for Y being set
for f being PartFunc of X,REAL st f is nonnegative holds
f | Y is nonnegative
proofend;

theorem Th56: :: MESFUNC6:56
for X being non empty set
for f, g being PartFunc of X,REAL st f is nonnegative &amp; g is nonnegative holds
f + g is nonnegative
proofend;

theorem :: MESFUNC6:57
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st f is nonnegative holds
( ( 0 <= r implies r (#) f is nonnegative ) &amp; ( r <= 0 implies r (#) f is nonpositive ) )
proofend;

theorem Th58: :: MESFUNC6:58
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in (dom f) /\ (dom g) holds
g . x <= f . x ) holds
f - g is nonnegative
proofend;

theorem :: MESFUNC6:59
for X being non empty set
for f, g, h being PartFunc of X,REAL st f is nonnegative &amp; g is nonnegative &amp; h is nonnegative holds
(f + g) + h is nonnegative
proofend;

theorem Th60: :: MESFUNC6:60
for X being non empty set
for f, g, h being PartFunc of X,REAL
for x being set st x in dom ((f + g) + h) holds
((f + g) + h) . x = ((f . x) + (g . x)) + (h . x)
proofend;

theorem :: MESFUNC6:61
for X being non empty set
for f being PartFunc of X,REAL holds
( max+ f is nonnegative &amp; max- f is nonnegative )
proofend;

theorem Th62: :: MESFUNC6:62
for X being non empty set
for f, g being PartFunc of X,REAL 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 :: MESFUNC6:63
for X being non empty set
for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)
proofend;

theorem :: MESFUNC6:64
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ (r (#) f) = r (#) (max+ f) &amp; max- (r (#) f) = r (#) (max- f) )
proofend;

theorem :: MESFUNC6:65
for X being non empty set
for f being PartFunc of X,REAL
for r being Real st 0 <= r holds
( max+ ((- r) (#) f) = r (#) (max- f) &amp; max- ((- r) (#) f) = r (#) (max+ f) )
proofend;

theorem :: MESFUNC6:66
for X being non empty set
for Y being set
for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y &amp; max- (f | Y) = (max- f) | Y )
proofend;

theorem :: MESFUNC6:67
for X being non empty set
for Y being set
for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y &amp; dom ((f | Y) + (g | Y)) = Y &amp; (f + g) | Y = (f | Y) + (g | Y) )
proofend;

theorem :: MESFUNC6:68
for X being non empty set
for f being PartFunc of X,REAL
for r being Real holds eq_dom (f,r) = f " {r}
proofend;

begin

theorem :: MESFUNC6:69
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
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))) /\ (less_dom (f,s)) in S
proofend;

theorem Th70: :: MESFUNC6:70
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
proofend;

theorem Th71: :: MESFUNC6:71
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL st f is_simple_func_in S holds
dom f is Element of S
proofend;

Lm1:  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,REAL 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 :: MESFUNC6:72
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL st f is_simple_func_in S &amp; g is_simple_func_in S holds
f + g is_simple_func_in S
proofend;

theorem :: MESFUNC6:73
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
proofend;

theorem :: MESFUNC6:74
for X being non empty set
for f, g being PartFunc of X,REAL st ( for x being set st x in dom (f - g) holds
g . x <= f . x ) holds
f - g is nonnegative
proofend;

theorem :: MESFUNC6:75
for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S &amp; dom f = A &amp; ( for x being set st x in A holds
f . x = r ) )
proofend;

theorem :: MESFUNC6:76
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B &amp; A = (dom f) /\ B holds
f | B is_measurable_on A
proofend;

theorem :: MESFUNC6:77
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= dom f &amp; f is_measurable_on A &amp; g is_measurable_on A holds
(max+ (f + g)) + (max- f) is_measurable_on A
proofend;

theorem :: MESFUNC6:78
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) &amp; f is_measurable_on A &amp; g is_measurable_on A holds
(max- (f + g)) + (max+ f) is_measurable_on A
proofend;

theorem :: MESFUNC6:79
for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL st dom f in S &amp; dom g in S holds
dom (f + g) in S
proofend;

theorem Th80: :: MESFUNC6:80
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL
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 :: MESFUNC6:81
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL 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
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,REAL;
func Integral (M,f) ->  Element of ExtREAL  equals :: MESFUNC6:def 3
 Integral (M,(R_EAL f));
coherence
 Integral (M,(R_EAL f)) is Element of ExtREAL ;
end;

:: deftheorem  defines Integral MESFUNC6:def_3_:_
 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,REAL holds Integral (M,f) = Integral (M,(R_EAL f));

theorem Th82: :: MESFUNC6: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,REAL 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,(R_EAL f))
proofend;

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

theorem :: MESFUNC6: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,REAL 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 :: MESFUNC6:85
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,REAL
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 :: MESFUNC6: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,REAL
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 :: MESFUNC6: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,REAL
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 :: MESFUNC6: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,REAL
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 :: MESFUNC6: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,REAL
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,REAL;
predf is_integrable_on M means :Def4: :: MESFUNC6:def 4
 R_EAL f is_integrable_on M;
end;

:: deftheorem Def4 defines is_integrable_on MESFUNC6:def_4_:_
 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,REAL holds
( f is_integrable_on M iff R_EAL f is_integrable_on M );

theorem :: MESFUNC6: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,REAL st f is_integrable_on M holds
( -infty < Integral (M,f) &amp; Integral (M,f) < +infty )
proofend;

theorem :: MESFUNC6: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,REAL
for A being Element of S st f is_integrable_on M holds
f | A is_integrable_on M
proofend;

theorem :: MESFUNC6: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,REAL
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 :: MESFUNC6: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,REAL
for B, A 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 :: MESFUNC6: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,REAL st ex A being Element of S st
( A = dom f &amp; f is_measurable_on A ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
proofend;

theorem :: MESFUNC6: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,REAL st f is_integrable_on M holds
|.(Integral (M,f)).| <= Integral (M,(abs f))
proofend;

theorem :: MESFUNC6:96
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,REAL 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
abs (f . x) <= g . x ) holds
( f is_integrable_on M &amp; Integral (M,(abs f)) <= Integral (M,g) )
proofend;

theorem :: MESFUNC6: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,REAL
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 :: MESFUNC6:98
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,REAL 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 :: MESFUNC6:99
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,REAL st f is_integrable_on M &amp; g is_integrable_on M holds
dom (f + g) in S
proofend;

theorem :: MESFUNC6:100
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,REAL st f is_integrable_on M &amp; g is_integrable_on M holds
f + g is_integrable_on M
proofend;

theorem :: MESFUNC6:101
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,REAL 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 :: MESFUNC6:102
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,REAL
for r being Real st f is_integrable_on M holds
( r (#) f is_integrable_on M &amp; Integral (M,(r (#) f)) = (R_EAL r) * (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,REAL;
let B be Element of S;
func Integral_on (M,B,f) ->  Element of ExtREAL  equals :: MESFUNC6:def 5
 Integral (M,(f | B));
coherence
 Integral (M,(f | B)) is Element of ExtREAL ;
end;

:: deftheorem  defines Integral_on MESFUNC6:def_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,REAL
for B being Element of S holds Integral_on (M,B,f) = Integral (M,(f | B));

theorem :: MESFUNC6:103
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,REAL
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 :: MESFUNC6: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,REAL
for r 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,(r (#) f)) = (R_EAL r) * (Integral_on (M,B,f)) )
proofend;