:: Fubini's Theorem for Nonnegative or Nonpositive Functions
:: by Noboru Endou
::
:: Copyright (c) 2018-2021 Association of Mizar Users

definition
let A, X be set ;
let er be ExtReal;
func chi (er,A,X) -> Function of X,ExtREAL means :Def1: :: MESFUN12:def 1
for x being object st x in X holds
( ( x in A implies it . x = er ) & ( not x in A implies it . x = 0 ) );
existence
ex b1 being Function of X,ExtREAL st
for x being object st x in X holds
( ( x in A implies b1 . x = er ) & ( not x in A implies b1 . x = 0 ) )
proof end;
uniqueness
for b1, b2 being Function of X,ExtREAL st ( for x being object st x in X holds
( ( x in A implies b1 . x = er ) & ( not x in A implies b1 . x = 0 ) ) ) & ( for x being object st x in X holds
( ( x in A implies b2 . x = er ) & ( not x in A implies b2 . x = 0 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines chi MESFUN12:def 1 :
for A, X being set
for er being ExtReal
for b4 being Function of X,ExtREAL holds
( b4 = chi (er,A,X) iff for x being object st x in X holds
( ( x in A implies b4 . x = er ) & ( not x in A implies b4 . x = 0 ) ) );

theorem Th1: :: MESFUN12:1
for X being non empty set
for A being set
for r being Real holds r (#) (chi (A,X)) = chi (r,A,X)
proof end;

theorem Th2: :: MESFUN12:2
for X being non empty set
for A being set holds
( chi (+infty,A,X) = Xchi (A,X) & chi (-infty,A,X) = - (Xchi (A,X)) )
proof end;

theorem Th3: :: MESFUN12:3
for X, A being set holds
( chi (A,X) is without+infty & chi (A,X) is without-infty )
proof end;

theorem Th4: :: MESFUN12:4
for X being non empty set
for A being set
for r being Real holds
( rng (chi (r,A,X)) c= {0,r} & chi (r,A,X) is V121() & chi (r,A,X) is V120() )
proof end;

theorem Th5: :: MESFUN12:5
for X being non empty set
for S being SigmaField of X
for f being non empty PartFunc of X,ExtREAL
for M being sigma_Measure of S st f is_simple_func_in S holds
ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) )
proof end;

definition
let F be FinSequence-like Function;
redefine attr F is disjoint_valued means :Def2: :: MESFUN12:def 2
for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n;
compatibility
( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n )
proof end;
end;

:: deftheorem Def2 defines disjoint_valued MESFUN12:def 2 :
for F being FinSequence-like Function holds
( F is disjoint_valued iff for m, n being Nat st m in dom F & n in dom F & m <> n holds
F . m misses F . n );

theorem Th6: :: MESFUN12:6
for X being non empty set
for S being SigmaField of X
for E1, E2 being Element of S st E1 misses E2 holds
<*E1,E2*> is Finite_Sep_Sequence of S
proof end;

theorem Th7: :: MESFUN12:7
for X being non empty set
for A1, A2 being Subset of X
for r1, r2 being Real holds <*(chi (r1,A1,X)),(chi (r2,A2,X))*> is summable FinSequence of Funcs (X,ExtREAL)
proof end;

theorem Th8: :: MESFUN12:8
for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL) st len F >= 2 holds
() /. 2 = (F /. 1) + (F /. 2)
proof end;

theorem Th9: :: MESFUN12:9
for X being non empty set
for f being Function of X,ExtREAL holds f + () = f
proof end;

theorem Th10: :: MESFUN12:10
for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL) holds
( dom F = dom () & ( for n being Nat st n in dom F holds
() /. n = () . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
(() /. (n + 1)) . x = ((() /. n) . x) + ((F /. (n + 1)) . x) ) )
proof end;

theorem Th11: :: MESFUN12:11
for X being non empty set
for S being SigmaField of X
for f being Function of X,ExtREAL
for E being Finite_Sep_Sequence of S
for F being summable FinSequence of Funcs (X,ExtREAL) st dom E = dom F & dom f = union (rng E) & ( for n being Nat st n in dom F holds
ex r being Real st F /. n = r (#) (chi ((E . n),X)) ) & f = () /. (len F) holds
( ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & m <> n holds
(F /. n) . x = 0 ) & ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n < m holds
(() /. n) . x = 0 ) & ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n >= m holds
(() /. n) . x = f . x ) & ( for x being Element of X
for m being Nat st m in dom F & x in E . m holds
(F /. m) . x = f . x ) & f is_simple_func_in S )
proof end;

theorem Th12: :: MESFUN12:12
for X being non empty set
for S being SigmaField of X
for E being Element of S holds chi (E,X) is_simple_func_in S
proof end;

theorem Th13: :: MESFUN12:13
for X being non empty set
for S being SigmaField of X
for A, B being Element of S
for er being ExtReal holds chi (er,A,X) is B -measurable
proof end;

theorem Th14: :: MESFUN12:14
for X being set
for A1, A2 being Subset of X
for er being ExtReal holds (chi (er,A1,X)) | A2 = (chi (er,(A1 /\ A2),X)) | A2
proof end;

theorem Th15: :: MESFUN12:15
for X being non empty set
for S being SigmaField of X
for A, B, C being Element of S
for er being ExtReal st C c= B holds
(chi (er,A,X)) | B is C -measurable
proof end;

theorem Th16: :: MESFUN12:16
for X being set
for A1, A2 being Subset of X
for er being ExtReal
for x being object st A1 misses A2 holds
((chi (er,A1,X)) | A2) . x = 0
proof end;

theorem Th17: :: MESFUN12:17
for X being set
for A being Subset of X
for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
proof end;

theorem Th18: :: MESFUN12:18
for A, X being set
for B being Subset of X holds dom ((chi (A,X)) | B) = B
proof end;

theorem Th19: :: MESFUN12:19
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is empty holds
f is_simple_func_in S
proof end;

theorem Th20: :: MESFUN12:20
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S holds Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
proof end;

theorem Th21: :: MESFUN12:21
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is E1 -measurable & E2 = dom g & g is nonnegative & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
proof end;

theorem Th22: :: MESFUN12:22
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
proof end;

theorem :: MESFUN12:23
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
proof end;

Lm1: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonnegative & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))

proof end;

Lm2: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & f is nonpositive & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f))

proof end;

theorem :: MESFUN12:24
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,ExtREAL
for r being Real st E = dom f & ( f is nonpositive or f is nonnegative ) & f is E -measurable holds
Integral (M,(r (#) f)) = r * (Integral (M,f)) by ;

theorem Th25: :: MESFUN12:25
for X, Y being non empty set
for A being Element of bool [:X,Y:]
for x, y being set st x in X & y in Y holds
( ( [x,y] in A implies x in Y-section (A,y) ) & ( x in Y-section (A,y) implies [x,y] in A ) & ( [x,y] in A implies y in X-section (A,x) ) & ( y in X-section (A,x) implies [x,y] in A ) )
proof end;

definition
let X1, X2 be non empty set ;
let Y be set ;
let f be PartFunc of [:X1,X2:],Y;
let x be Element of X1;
func ProjPMap1 (f,x) -> PartFunc of X2,Y means :Def3: :: MESFUN12:def 3
( dom it = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
it . y = f . (x,y) ) );
existence
ex b1 being PartFunc of X2,Y st
( dom b1 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
b1 . y = f . (x,y) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of X2,Y st dom b1 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
b1 . y = f . (x,y) ) & dom b2 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
b2 . y = f . (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ProjPMap1 MESFUN12:def 3 :
for X1, X2 being non empty set
for Y being set
for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for b6 being PartFunc of X2,Y holds
( b6 = ProjPMap1 (f,x) iff ( dom b6 = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
b6 . y = f . (x,y) ) ) );

definition
let X1, X2 be non empty set ;
let Y be set ;
let f be PartFunc of [:X1,X2:],Y;
let y be Element of X2;
func ProjPMap2 (f,y) -> PartFunc of X1,Y means :Def4: :: MESFUN12:def 4
( dom it = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
it . x = f . (x,y) ) );
existence
ex b1 being PartFunc of X1,Y st
( dom b1 = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
b1 . x = f . (x,y) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of X1,Y st dom b1 = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
b1 . x = f . (x,y) ) & dom b2 = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
b2 . x = f . (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines ProjPMap2 MESFUN12:def 4 :
for X1, X2 being non empty set
for Y being set
for f being PartFunc of [:X1,X2:],Y
for y being Element of X2
for b6 being PartFunc of X1,Y holds
( b6 = ProjPMap2 (f,y) iff ( dom b6 = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
b6 . x = f . (x,y) ) ) );

theorem Th26: :: MESFUN12:26
for X1, X2 being non empty set
for Y being set
for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
proof end;

theorem Th27: :: MESFUN12:27
for X1, X2, Y being non empty set
for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )
proof end;

theorem :: MESFUN12:28
for X, Y, Z being non empty set
for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y
for A being set holds
( X-section ((f " A),x) = (ProjPMap1 (f,x)) " A & Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A )
proof end;

theorem Th29: :: MESFUN12:29
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
proof end;

theorem :: MESFUN12:30
for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2 st ( for z being Element of [:X1,X2:] st z in dom f holds
f . z = 0 ) holds
( (ProjPMap2 (f,y)) . x = 0 & (ProjPMap1 (f,x)) . y = 0 )
proof end;

theorem Th31: :: MESFUN12:31
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap2 (f,y) is_simple_func_in S1 )
proof end;

theorem Th32: :: MESFUN12:32
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds
( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )
proof end;

theorem Th33: :: MESFUN12:33
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds
( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )
proof end;

theorem Th34: :: MESFUN12:34
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for A being Subset of [:X1,X2:]
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) )
proof end;

theorem Th35: :: MESFUN12:35
for X1, X2 being non empty set
for A being Subset of [:X1,X2:]
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )
proof end;

theorem Th36: :: MESFUN12:36
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 E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is E -measurable holds
g is E -measurable
proof end;

theorem Th37: :: MESFUN12:37
for X1, X2 being non empty set
for A being Subset of [:X1,X2:]
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for F being Functional_Sequence of [:X1,X2:],ExtREAL st A c= dom f & ( for n being Nat holds dom (F . n) = A ) & ( for z being Element of [:X1,X2:] st z in A holds
( F # z is convergent & lim (F # z) = f . z ) ) holds
( ex FX being with_the_same_dom Functional_Sequence of X1,ExtREAL st
( ( for n being Nat holds FX . n = ProjPMap2 ((F . n),y) ) & ( for x being Element of X1 st x in Y-section (A,y) holds
( FX # x is convergent & (ProjPMap2 (f,y)) . x = lim (FX # x) ) ) ) & ex FY being with_the_same_dom Functional_Sequence of X2,ExtREAL st
( ( for n being Nat holds FY . n = ProjPMap1 ((F . n),x) ) & ( for y being Element of X2 st y in X-section (A,x) holds
( FY # y is convergent & (ProjPMap1 (f,x)) . y = lim (FY # y) ) ) ) )
proof end;

Lm3: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for A being Element of sigma (measurable_rectangles (S1,S2)) st ( f is nonnegative or f is nonpositive ) & A c= dom f & f is A -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable )

proof end;

theorem :: MESFUN12:38
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for M2 being sigma_Measure of S2
for A being Element of S1
for B being Element of S2
for x being Element of X1 holds (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)))
proof end;

theorem :: MESFUN12:39
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for M1 being sigma_Measure of S1
for A being Element of S1
for B being Element of S2
for y being Element of X2 holds (M1 . (A /\ (Measurable-Y-section (E,y)))) * ((chi (B,X2)) . y) = Integral (M1,(ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)))
proof end;

theorem Th40: :: MESFUN12:40
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for er being ExtReal holds
( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )
proof end;

theorem Th41: :: MESFUN12:41
for X1, X2 being non empty set
for A, Z being set
for f being PartFunc of [:X1,X2:],Z
for x being Element of X1 holds X-section ((f " A),x) = (ProjPMap1 (f,x)) " A
proof end;

theorem Th42: :: MESFUN12:42
for X1, X2 being non empty set
for A, Z being set
for f being PartFunc of [:X1,X2:],Z
for y being Element of X2 holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A
proof end;

theorem Th43: :: MESFUN12:43
for X1, X2 being non empty set
for A, B being Subset of [:X1,X2:]
for p being set holds
( X-section ((A \ B),p) = (X-section (A,p)) \ (X-section (B,p)) & Y-section ((A \ B),p) = (Y-section (A,p)) \ (Y-section (B,p)) )
proof end;

theorem Th44: :: MESFUN12:44
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f1, f2 being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f1 + f2),x) = (ProjPMap1 (f1,x)) + (ProjPMap1 (f2,x)) & ProjPMap1 ((f1 - f2),x) = (ProjPMap1 (f1,x)) - (ProjPMap1 (f2,x)) & ProjPMap2 ((f1 + f2),y) = (ProjPMap2 (f1,y)) + (ProjPMap2 (f2,y)) & ProjPMap2 ((f1 - f2),y) = (ProjPMap2 (f1,y)) - (ProjPMap2 (f2,y)) )
proof end;

Lm4: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E c= dom f & f is E -measurable holds
( ProjPMap1 ((max+ f),x) is Measurable-X-section (E,x) -measurable & ProjPMap2 ((max+ f),y) is Measurable-Y-section (E,y) -measurable & ProjPMap1 ((max- f),x) is Measurable-X-section (E,x) -measurable & ProjPMap2 ((max- f),y) is Measurable-Y-section (E,y) -measurable )

proof end;

theorem Th45: :: MESFUN12:45
for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1 holds
( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )
proof end;

theorem Th46: :: MESFUN12:46
for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for y being Element of X2 holds
( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )
proof end;

theorem Th47: :: MESFUN12:47
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st E c= dom f & f is E -measurable holds
( ProjPMap1 (f,x) is Measurable-X-section (E,x) -measurable & ProjPMap2 (f,y) is Measurable-Y-section (E,y) -measurable )
proof end;

definition
let X1, X2, Y be non empty set ;
let F be Functional_Sequence of [:X1,X2:],Y;
let x be Element of X1;
func ProjPMap1 (F,x) -> Functional_Sequence of X2,Y means :Def5: :: MESFUN12:def 5
for n being Nat holds it . n = ProjPMap1 ((F . n),x);
existence
ex b1 being Functional_Sequence of X2,Y st
for n being Nat holds b1 . n = ProjPMap1 ((F . n),x)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X2,Y st ( for n being Nat holds b1 . n = ProjPMap1 ((F . n),x) ) & ( for n being Nat holds b2 . n = ProjPMap1 ((F . n),x) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines ProjPMap1 MESFUN12:def 5 :
for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for x being Element of X1
for b6 being Functional_Sequence of X2,Y holds
( b6 = ProjPMap1 (F,x) iff for n being Nat holds b6 . n = ProjPMap1 ((F . n),x) );

definition
let X1, X2, Y be non empty set ;
let F be Functional_Sequence of [:X1,X2:],Y;
let y be Element of X2;
func ProjPMap2 (F,y) -> Functional_Sequence of X1,Y means :Def6: :: MESFUN12:def 6
for n being Nat holds it . n = ProjPMap2 ((F . n),y);
existence
ex b1 being Functional_Sequence of X1,Y st
for n being Nat holds b1 . n = ProjPMap2 ((F . n),y)
proof end;
uniqueness
for b1, b2 being Functional_Sequence of X1,Y st ( for n being Nat holds b1 . n = ProjPMap2 ((F . n),y) ) & ( for n being Nat holds b2 . n = ProjPMap2 ((F . n),y) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ProjPMap2 MESFUN12:def 6 :
for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for y being Element of X2
for b6 being Functional_Sequence of X1,Y holds
( b6 = ProjPMap2 (F,y) iff for n being Nat holds b6 . n = ProjPMap2 ((F . n),y) );

theorem Th48: :: MESFUN12:48
for X1, X2 being non empty set
for E being Subset of [:X1,X2:]
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )
proof end;

theorem Th49: :: MESFUN12:49
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for er being ExtReal holds Integral (M,(chi (er,E,X))) = er * (M . E)
proof end;

theorem Th50: :: MESFUN12:50
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for er being ExtReal holds Integral (M,((chi (er,E,X)) | E)) = er * (M . E)
proof end;

theorem :: MESFUN12:51
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S
for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
proof end;

theorem Th52: :: MESFUN12:52
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
( (Y-vol (E,M2)) . x = Integral (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral+ (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) & (Y-vol (E,M2)) . x = integral' (M2,(ProjPMap1 ((chi (E,[:X1,X2:])),x))) )
proof end;

theorem Th53: :: MESFUN12:53
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
( (X-vol (E,M1)) . y = Integral (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral+ (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) & (X-vol (E,M1)) . y = integral' (M1,(ProjPMap2 ((chi (E,[:X1,X2:])),y))) )
proof end;

theorem :: MESFUN12:54
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for r being Real holds Integral (M,(r (#) (chi (E,X)))) = r * (Integral (M,(chi (E,X))))
proof end;

theorem Th55: :: MESFUN12:55
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite holds
( (r (#) (X-vol (E,M1))) . y = Integral (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) & ( r >= 0 implies (r (#) (X-vol (E,M1))) . y = integral+ (M1,(ProjPMap2 ((chi (r,E,[:X1,X2:])),y))) ) )
proof end;

theorem Th56: :: MESFUN12:56
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M2 is sigma_finite holds
( (r (#) (Y-vol (E,M2))) . x = Integral (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) & ( r >= 0 implies (r (#) (Y-vol (E,M2))) . x = integral+ (M2,(ProjPMap1 ((chi (r,E,[:X1,X2:])),x))) ) )
proof end;

theorem Th57: :: MESFUN12:57
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 dom f in S & ( for x being Element of X st x in dom f holds
0 = f . x ) holds
( ( for E being Element of S st E c= dom f holds
f is E -measurable ) & Integral (M,f) = 0 )
proof end;

Lm5: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )

proof end;

Lm6: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )

proof end;

theorem Th58: :: MESFUN12:58
for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 st F is with_the_same_dom holds
( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )
proof end;

Lm7: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )

proof end;

Lm8: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable holds
ex I1 being Function of X2,ExtREAL st
( ( for y being Element of X2 holds I1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for V being Element of S2 holds I1 is V -measurable ) )

proof end;

Lm9: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )

proof end;

Lm10: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M2 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable holds
ex I2 being Function of X1,ExtREAL st
( ( for x being Element of X1 holds I2 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for V being Element of S1 holds I2 is V -measurable ) )

proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let M1 be sigma_Measure of S1;
let f be PartFunc of [:X1,X2:],ExtREAL;
func Integral1 (M1,f) -> Function of X2,ExtREAL means :Def7: :: MESFUN12:def 7
for y being Element of X2 holds it . y = Integral (M1,(ProjPMap2 (f,y)));
existence
ex b1 being Function of X2,ExtREAL st
for y being Element of X2 holds b1 . y = Integral (M1,(ProjPMap2 (f,y)))
proof end;
uniqueness
for b1, b2 being Function of X2,ExtREAL st ( for y being Element of X2 holds b1 . y = Integral (M1,(ProjPMap2 (f,y))) ) & ( for y being Element of X2 holds b2 . y = Integral (M1,(ProjPMap2 (f,y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Integral1 MESFUN12:def 7 :
for X1, X2 being non empty set
for S1 being SigmaField of X1
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for b6 being Function of X2,ExtREAL holds
( b6 = Integral1 (M1,f) iff for y being Element of X2 holds b6 . y = Integral (M1,(ProjPMap2 (f,y))) );

definition
let X1, X2 be non empty set ;
let S2 be SigmaField of X2;
let M2 be sigma_Measure of S2;
let f be PartFunc of [:X1,X2:],ExtREAL;
func Integral2 (M2,f) -> Function of X1,ExtREAL means :Def8: :: MESFUN12:def 8
for x being Element of X1 holds it . x = Integral (M2,(ProjPMap1 (f,x)));
existence
ex b1 being Function of X1,ExtREAL st
for x being Element of X1 holds b1 . x = Integral (M2,(ProjPMap1 (f,x)))
proof end;
uniqueness
for b1, b2 being Function of X1,ExtREAL st ( for x being Element of X1 holds b1 . x = Integral (M2,(ProjPMap1 (f,x))) ) & ( for x being Element of X1 holds b2 . x = Integral (M2,(ProjPMap1 (f,x))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Integral2 MESFUN12:def 8 :
for X1, X2 being non empty set
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for b6 being Function of X1,ExtREAL holds
( b6 = Integral2 (M2,f) iff for x being Element of X1 holds b6 . x = Integral (M2,(ProjPMap1 (f,x))) );

theorem Th59: :: MESFUN12:59
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is E -measurable holds
Integral1 (M1,f) is V -measurable
proof end;

theorem Th60: :: MESFUN12:60
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E = dom f & f is E -measurable holds
Integral2 (M2,f) is U -measurable
proof end;

theorem Th61: :: MESFUN12:61
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for y being Element of X2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
(X-vol (E,M1)) . y = Integral (M1,(chi ((Measurable-Y-section (E,y)),X1)))
proof end;

theorem Th62: :: MESFUN12:62
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for x being Element of X1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
(Y-vol (E,M2)) . x = Integral (M2,(chi ((Measurable-X-section (E,x)),X2)))
proof end;

theorem Th63: :: MESFUN12:63
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )
proof end;

theorem Th64: :: MESFUN12:64
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite holds
X-vol (E,M1) = Integral1 (M1,(chi (E,[:X1,X2:])))
proof end;

theorem Th65: :: MESFUN12:65
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite holds
Y-vol (E,M2) = Integral2 (M2,(chi (E,[:X1,X2:])))
proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let M1 be sigma_Measure of S1;
let M2 be sigma_Measure of S2;
func Prod_Measure (M1,M2) -> sigma_Measure of (sigma (measurable_rectangles (S1,S2))) equals :: MESFUN12:def 9
product_sigma_Measure (M1,M2);
correctness
coherence
product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))
;
by MEASUR11:8;
end;

:: deftheorem defines Prod_Measure MESFUN12:def 9 :
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 holds Prod_Measure (M1,M2) = product_sigma_Measure (M1,M2);

theorem Th66: :: MESFUN12:66
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable holds
( Integral1 (M1,f) is V112() & Integral1 (M1,(f | E2)) is V112() & Integral2 (M2,f) is V112() & Integral2 (M2,(f | E2)) is V112() )
proof end;

theorem Th67: :: MESFUN12:67
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable holds
( Integral1 (M1,f) is nonpositive & Integral1 (M1,(f | E2)) is nonpositive & Integral2 (M2,f) is nonpositive & Integral2 (M2,(f | E2)) is nonpositive )
proof end;

theorem Th68: :: MESFUN12:68
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2))
for V being Element of S2 st M1 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is E1 -measurable holds
Integral1 (M1,(f | E2)) is V -measurable
proof end;

theorem Th69: :: MESFUN12:69
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2))
for U being Element of S1 st M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & E1 = dom f & f is E1 -measurable holds
Integral2 (M2,(f | E2)) is U -measurable
proof end;

theorem :: MESFUN12:70
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for x being Element of X1 st x in dom (ProjPMap2 (f,y)) holds
(ProjPMap2 (f,y)) . x = 0 ) holds
(Integral1 (M1,f)) . y = 0
proof end;

theorem :: MESFUN12:71
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & ( for y being Element of X2 st y in dom (ProjPMap1 (f,x)) holds
(ProjPMap1 (f,x)) . y = 0 ) holds
(Integral2 (M2,f)) . x = 0
proof end;

Lm11: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )

proof end;

Lm12: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonpositive & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )

proof end;

theorem :: MESFUN12:72
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, E1, E2 being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable & E1 misses E2 holds
( Integral1 (M1,(f | (E1 \/ E2))) = (Integral1 (M1,(f | E1))) + (Integral1 (M1,(f | E2))) & Integral2 (M2,(f | (E1 \/ E2))) = (Integral2 (M2,(f | E1))) + (Integral2 (M2,(f | E2))) ) by ;

theorem Th73: :: MESFUN12:73
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for E being Element of sigma (measurable_rectangles (S1,S2)) st E = dom f & f is E -measurable holds
( Integral1 (M1,(- f)) = - (Integral1 (M1,f)) & Integral2 (M2,(- f)) = - (Integral2 (M2,f)) )
proof end;

theorem Th74: :: MESFUN12:74
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable & E2 = dom g & g is nonnegative & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
proof end;

theorem :: MESFUN12:75
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) & Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) )
proof end;

theorem :: MESFUN12:76
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f, g being PartFunc of [:X1,X2:],ExtREAL
for E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 = dom f & f is nonnegative & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
( Integral1 (M1,(f - g)) = (Integral1 (M1,(f | (dom (f - g))))) - (Integral1 (M1,(g | (dom (f - g))))) & Integral1 (M1,(g - f)) = (Integral1 (M1,(g | (dom (g - f))))) - (Integral1 (M1,(f | (dom (g - f))))) & Integral2 (M2,(f - g)) = (Integral2 (M2,(f | (dom (f - g))))) - (Integral2 (M2,(g | (dom (f - g))))) & Integral2 (M2,(g - f)) = (Integral2 (M2,(g | (dom (g - f))))) - (Integral2 (M2,(f | (dom (g - f))))) )
proof end;

theorem Th77: :: MESFUN12:77
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
( Integral (M1,(Y-vol (E,M2))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) & Integral (M2,(X-vol (E,M1))) = Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) )
proof end;

theorem Th78: :: MESFUN12:78
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL
for r being Real st E = dom f & ( f is nonnegative or f is nonpositive ) & f is E -measurable holds
( Integral1 (M1,(r (#) f)) = r (#) (Integral1 (M1,f)) & Integral2 (M2,(r (#) f)) = r (#) (Integral2 (M2,f)) )
proof end;

theorem Th79: :: MESFUN12:79
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )
proof end;

theorem Th80: :: MESFUN12:80
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
proof end;

theorem Th81: :: MESFUN12:81
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
proof end;

theorem Th82: :: MESFUN12:82
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (E,[:X1,X2:])) | E)))) )
proof end;

theorem Th83: :: MESFUN12:83
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
proof end;

Lm13: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )

proof end;

Lm14: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )

proof end;

Lm15: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )

proof end;

Lm16: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))

proof end;

Lm17: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonnegative & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))

proof end;

Lm18: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))

proof end;

Lm19: for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & f is nonpositive & A = dom f & f is A -measurable holds
Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))

proof end;

theorem :: MESFUN12:84
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for A being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st M1 is sigma_finite & M2 is sigma_finite & ( f is nonnegative or f is nonpositive ) & A = dom f & f is A -measurable holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) by ;