:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Copyright (c) 2006-2021 Association of Mizar Users

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

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 object st x in dom f holds
f . x = r ) holds
f is_simple_func_in S
proof end;

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

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

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 & ex y being Real st
( y = f . x & r < y ) ) )
proof end;

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 & ex y being Real st
( y = f . x & r <= y ) ) )
proof end;

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 & ex y being Real st
( y = f . x & r = y ) ) )
proof end;

theorem :: MESFUNC6:8
for X being non empty set
for Y being set
for S being SigmaField of X
for F being sequence of 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)
proof end;

theorem :: MESFUNC6:9
for X being non empty set
for Y being set
for S being SigmaField of X
for F being sequence of 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)
proof end;

theorem :: MESFUNC6:10
for X being non empty set
for Y being set
for S being SigmaField of X
for F being sequence of 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)
proof end;

theorem :: MESFUNC6:11
for X being non empty set
for Y being set
for S being SigmaField of X
for F being sequence of 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)
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let A be Element of S;
let f be PartFunc of X,REAL;
attr f is A -measurable means :: MESFUNC6:def 1
R_EAL f is A -measurable ;
end;

:: deftheorem defines -measurable MESFUNC6:def 1 :
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL holds
( f is A -measurable iff R_EAL f is A -measurable );

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 A -measurable iff for r being Real holds A /\ (less_dom (f,r)) in S ) by MESFUNC1:def 16;

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 A -measurable iff for r being Real holds A /\ (great_eq_dom (f,r)) in S ) by MESFUNC1:27;

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 A -measurable iff for r being Real holds A /\ (less_eq_dom (f,r)) in S ) by MESFUNC1:28;

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 A -measurable iff for r being Real holds A /\ (great_dom (f,r)) in S ) by MESFUNC1:29;

theorem :: MESFUNC6:16
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 B c= A & f is A -measurable holds
f is B -measurable by MESFUNC1:30;

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 A -measurable & f is B -measurable holds
f is A \/ B -measurable by MESFUNC1:31;

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 A -measurable & A c= dom f holds
(A /\ (great_dom (f,r))) /\ (less_dom (f,s)) in S by MESFUNC1:32;

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 A -measurable & g is A -measurable & A c= dom g holds
(A /\ (less_dom (f,r))) /\ (great_dom (g,r)) in S by MESFUNC1:36;

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 (#) ()
proof end;

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 A -measurable & A c= dom f holds
r (#) f is A -measurable
proof end;

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

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 - g) = () - () & dom (R_EAL (f + g)) = (dom ()) /\ (dom ()) & dom (R_EAL (f - g)) = (dom ()) /\ (dom ()) & dom (R_EAL (f + g)) = (dom f) /\ (dom g) & dom (R_EAL (f - g)) = (dom f) /\ (dom g) )
proof end;

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)
proof end;

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 A -measurable & g is A -measurable 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)))) by MESFUNC2:6;

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 A -measurable & g is A -measurable holds
f + g is A -measurable
proof end;

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

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

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 A -measurable & g is A -measurable & A c= dom g holds
f - g is A -measurable
proof end;

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

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
proof end;

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
proof end;

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

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 & 0 < (max+ f) . x holds
(max- f) . x = 0
proof end;

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 & 0 < (max- f) . x holds
(max+ f) . x = 0
proof end;

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

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 ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0 ) )
proof end;

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 & (max+ f) . x = f . x holds
(max- f) . x = 0
proof end;

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 & (max+ f) . x = 0 holds
(max- f) . x = - (f . x)
proof end;

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 & (max- f) . x = - (f . x) holds
(max+ f) . x = 0
proof end;

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 & (max- f) . x = 0 holds
(max+ f) . x = f . x
proof end;

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

theorem Th43: :: MESFUNC6:43
for r being Real holds |.r.| = |.r.|
proof end;

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

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

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 A -measurable holds
max+ f is A -measurable
proof end;

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 A -measurable & A c= dom f holds
max- f is A -measurable
proof end;

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 A -measurable & A c= dom f holds
abs f is A -measurable
proof end;

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

:: deftheorem 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) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & 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 ) by MESFUNC2:def 4;

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 A -measurable by ;

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

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

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 )
proof end;

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

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
proof end;

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

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 ) & ( r <= 0 implies r (#) f is nonpositive ) )
proof end;

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
proof end;

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

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

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

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) & dom ((max- (f + g)) + (max+ f)) = (dom f) /\ (dom g) & dom (((max+ (f + g)) + (max- f)) + (max- g)) = (dom f) /\ (dom g) & dom (((max- (f + g)) + (max+ f)) + (max+ g)) = (dom f) /\ (dom g) & (max+ (f + g)) + (max- f) is nonnegative & (max- (f + g)) + (max+ f) is nonnegative )
proof end;

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)
proof end;

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) & max- (r (#) f) = r (#) (max- f) )
proof end;

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) & max- ((- r) (#) f) = r (#) (max+ f) )
proof end;

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 & max- (f | Y) = (max- f) | Y )
proof end;

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 & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
proof end;

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}
proof end;

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 A -measurable & A c= dom f holds
(A /\ (great_eq_dom (f,r))) /\ (less_dom (f,s)) in S
proof end;

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
proof end;

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 by MESFUNC2:31;

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

proof end;

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 & g is_simple_func_in S holds
f + g is_simple_func_in S
proof end;

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
proof end;

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
proof end;

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 & dom f = A & ( for x being object st x in A holds
f . x = r ) )
proof end;

theorem :: MESFUNC6:76
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 B -measurable & A = (dom f) /\ B holds
f | B is A -measurable
proof end;

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 & f is A -measurable & g is A -measurable holds
(max+ (f + g)) + (max- f) is A -measurable
proof end;

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) & f is A -measurable & g is A -measurable holds
(max- (f + g)) + (max+ f) is A -measurable
proof end;

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 & dom g in S holds
dom (f + g) in S
proof end;

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 B -measurable iff f is A /\ B -measurable )
proof end;

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 B -measurable holds
c (#) f is B -measurable
proof end;

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,());
coherence
Integral (M,()) 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,());

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 & f is A -measurable ) & f is nonnegative holds
Integral (M,f) = integral+ (M,()) by MESFUNC5:88;

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 & f is nonnegative holds
( Integral (M,f) = integral+ (M,()) & Integral (M,f) = integral' (M,()) )
proof end;

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

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 & f is E -measurable ) & f is nonnegative & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:91;

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 & f is E -measurable ) & f is nonnegative holds
0 <= Integral (M,(f | A)) by MESFUNC5:92;

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 & f is E -measurable ) & f is nonnegative & A c= B holds
Integral (M,(f | A)) <= Integral (M,(f | B)) by MESFUNC5:93;

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 & f is E -measurable ) & M . A = 0 holds
Integral (M,(f | A)) = 0 by MESFUNC5:94;

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 & f is E -measurable & M . A = 0 holds
Integral (M,(f | (E \ A))) = Integral (M,f) by MESFUNC5:95;

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;
end;

:: deftheorem 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) & Integral (M,f) < +infty ) by MESFUNC5:96;

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 by MESFUNC5:97;

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 & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by MESFUNC5:98;

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

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 & f is A -measurable ) holds
( f is_integrable_on M iff abs f is_integrable_on M )
proof end;

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))
proof end;

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 & f is A -measurable ) & dom f = dom g & g is_integrable_on M & ( for x being Element of X st x in dom f holds
|.(f . x).| <= g . x ) holds
( f is_integrable_on M & Integral (M,(abs f)) <= Integral (M,g) )
proof end;

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 & 0 <= r & ( for x being object st x in dom f holds
f . x = r ) holds
Integral (M,f) = r * (M . (dom f))
proof end;

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 & g is_integrable_on M & f is nonnegative & g is nonnegative holds
f + g is_integrable_on M
proof end;

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 & g is_integrable_on M holds
dom (f + g) in S
proof end;

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 & g is_integrable_on M holds
f + g is_integrable_on M
proof end;

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 & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) )
proof end;

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 & Integral (M,(r (#) f)) = r * (Integral (M,f)) )
proof end;

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 & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
proof end;

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 & Integral_on (M,B,(r (#) f)) = r * (Integral_on (M,B,f)) )
proof end;