MESFUN12: Fubini's Theorem for Nonnegative or Nonpositive Functions

:: Fubini's Theorem for Nonnegative or Nonpositive Functions
:: by Noboru Endou
::
:: Received March 27, 2018
:: 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 ) );

proof end;

proof end;

end;

:: deftheorem Def1 defines chi MESFUN12:def 1 :

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;

proof end;

end;

:: deftheorem Def2 defines disjoint_valued MESFUN12:def 2 :

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
(Partial_Sums F) /. 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 + (X --> 0.) = 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 (Partial_Sums F) & ( for n being Nat st n in dom F holds
(Partial_Sums F) /. n = (Partial_Sums F) . n ) & ( for n being Nat
for x being Element of X st 1 <= n & n < len F holds
((Partial_Sums F) /. (n + 1)) . x = (((Partial_Sums F) /. 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 = (Partial_Sums 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
((Partial_Sums 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
((Partial_Sums F) /. 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 Lm1, Lm2;

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

proof end;

proof end;

end;

:: deftheorem Def3 defines ProjPMap1 MESFUN12:def 3 :

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

proof end;

proof end;

end;

:: deftheorem Def4 defines ProjPMap2 MESFUN12:def 4 :

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

proof end;

proof end;

end;

:: deftheorem Def5 defines ProjPMap1 MESFUN12:def 5 :

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

proof end;

proof end;

end;

:: deftheorem Def6 defines ProjPMap2 MESFUN12:def 6 :

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

proof end;

proof end;

end;

:: deftheorem Def7 defines Integral1 MESFUN12:def 7 :

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

proof end;

proof end;

end;

:: deftheorem Def8 defines Integral2 MESFUN12:def 8 :

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 by MEASUR11:8;

end;

:: deftheorem defines Prod_Measure MESFUN12:def 9 :

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 Lm11, Lm12;

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 Lm16, Lm18, Lm17, Lm19;