:: Fubini's Theorem on Measure
:: by Noboru Endou
::
:: Received February 23, 2017
:: Copyright (c) 2017-2021 Association of Mizar Users


theorem Th72: :: MEASUR11:1
for F being disjoint_valued FinSequence
for n, m being Nat st n < m holds
union (rng (F | n)) misses F . m
proof end;

theorem Th73: :: MEASUR11:2
for F being FinSequence
for m, n being Nat st m <= n holds
len (F | m) <= len (F | n)
proof end;

theorem Th74: :: MEASUR11:3
for F being FinSequence
for n being Nat holds (union (rng (F | n))) \/ (F . (n + 1)) = union (rng (F | (n + 1)))
proof end;

theorem Th101: :: MEASUR11:4
for F being disjoint_valued FinSequence
for n being Nat holds Union (F | n) misses F . (n + 1)
proof end;

theorem Th41: :: MEASUR11:5
for P being set
for F being FinSequence st P is cup-closed & {} in P & ( for n being Nat st n in dom F holds
F . n in P ) holds
Union F in P
proof end;

definition
let A, X be set ;
:: original: chi
redefine func chi (A,X) -> Function of X,ExtREAL;
coherence
chi (A,X) is Function of X,ExtREAL
proof end;
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let F be FinSequence of S;
:: original: Union
redefine func Union F -> Element of S;
coherence
Union F is Element of S by PROB_3:57;
end;

definition
let X be non empty set ;
let S be SigmaField of X;
let F be sequence of S;
:: original: Union
redefine func Union F -> Element of S;
coherence
Union F is Element of S
proof end;
end;

definition
let X be non empty set ;
let F be FinSequence of PFuncs (X,ExtREAL);
let x be Element of X;
func F # x -> FinSequence of ExtREAL means :DEF5: :: MEASUR11:def 1
( dom it = dom F & ( for n being Element of NAT st n in dom it holds
it . n = (F . n) . x ) );
existence
ex b1 being FinSequence of ExtREAL st
( dom b1 = dom F & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (F . n) . x ) )
proof end;
uniqueness
for b1, b2 being FinSequence of ExtREAL st dom b1 = dom F & ( for n being Element of NAT st n in dom b1 holds
b1 . n = (F . n) . x ) & dom b2 = dom F & ( for n being Element of NAT st n in dom b2 holds
b2 . n = (F . n) . x ) holds
b1 = b2
proof end;
end;

:: deftheorem DEF5 defines # MEASUR11:def 1 :
for X being non empty set
for F being FinSequence of PFuncs (X,ExtREAL)
for x being Element of X
for b4 being FinSequence of ExtREAL holds
( b4 = F # x iff ( dom b4 = dom F & ( for n being Element of NAT st n in dom b4 holds
b4 . n = (F . n) . x ) ) );

theorem :: MEASUR11:6
for X being non empty set
for S being non empty Subset-Family of X
for f being FinSequence of S
for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) holds
for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)
proof end;

theorem Th1: :: MEASUR11:7
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2 holds sigma (DisUnion (measurable_rectangles (S1,S2))) = sigma (measurable_rectangles (S1,S2))
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 product_Measure (M1,M2) -> induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) means :: MEASUR11:def 2
 for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
it . E = Sum ((product-pre-Measure (M1,M2)) * F);
existence
ex b1 being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) st
for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
b1 . E = Sum ((product-pre-Measure (M1,M2)) * F)
proof end;
uniqueness
for b1, b2 being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) st ( for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
b1 . E = Sum ((product-pre-Measure (M1,M2)) * F) ) & ( for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
b2 . E = Sum ((product-pre-Measure (M1,M2)) * F) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines product_Measure MEASUR11:def 2 :
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 b7 being induced_Measure of measurable_rectangles (S1,S2), product-pre-Measure (M1,M2) holds
( b7 = product_Measure (M1,M2) iff for E being set st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) st E = Union F holds
b7 . E = Sum ((product-pre-Measure (M1,M2)) * F) );

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 product_sigma_Measure (M1,M2) -> induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2) equals :: MEASUR11:def 3
(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));
correctness
coherence
(sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2))) is induced_sigma_Measure of measurable_rectangles (S1,S2), product_Measure (M1,M2);
proof end;
end;

:: deftheorem defines product_sigma_Measure MEASUR11:def 3 :
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 product_sigma_Measure (M1,M2) = (sigma_Meas (C_Meas (product_Measure (M1,M2)))) | (sigma (measurable_rectangles (S1,S2)));

theorem Th2: :: MEASUR11:8
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 product_sigma_Measure (M1,M2) is sigma_Measure of (sigma (measurable_rectangles (S1,S2)))
proof end;

theorem Th3: :: MEASUR11:9
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds [:(F1 . n),(F2 . n):] is Element of sigma (measurable_rectangles (S1,S2))
proof end;

theorem Th4: :: MEASUR11:10
for X1, X2 being set
for F1 being SetSequence of X1
for F2 being SetSequence of X2
for n being Nat st F1 is non-descending & F2 is non-descending holds
[:(F1 . n),(F2 . n):] c= [:(F1 . (n + 1)),(F2 . (n + 1)):]
proof end;

theorem Th5: :: MEASUR11:11
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 S1
for B being Element of S2 holds (product_Measure (M1,M2)) . [:A,B:] = (M1 . A) * (M2 . B)
proof end;

theorem Th6: :: MEASUR11:12
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 F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
proof end;

theorem :: MEASUR11:13
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 F1 being FinSequence of S1
for F2 being FinSequence of S2
for n being Nat st n in dom F1 & n in dom F2 holds
(product_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n)) by Th5;

theorem :: MEASUR11:14
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 Subset of [:X1,X2:] holds (C_Meas (product_Measure (M1,M2))) . E = inf (Svc ((product_Measure (M1,M2)),E)) by MEASURE8:def 8;

theorem Th9: :: MEASUR11:15
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 sigma (measurable_rectangles (S1,S2)) c= sigma_Field (C_Meas (product_Measure (M1,M2)))
proof end;

theorem Th10: :: MEASUR11:16
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 A being Element of S1
for B being Element of S2 st E = [:A,B:] holds
(product_sigma_Measure (M1,M2)) . E = (M1 . A) * (M2 . B)
proof end;

theorem :: MEASUR11:17
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 F1 being Set_Sequence of S1
for F2 being Set_Sequence of S2
for n being Nat holds (product_sigma_Measure (M1,M2)) . [:(F1 . n),(F2 . n):] = (M1 . (F1 . n)) * (M2 . (F2 . n))
proof end;

theorem Th12: :: MEASUR11:18
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st E1 misses E2 holds
(product_sigma_Measure (M1,M2)) . (E1 \/ E2) = ((product_sigma_Measure (M1,M2)) . E1) + ((product_sigma_Measure (M1,M2)) . E2)
proof end;

theorem :: MEASUR11:19
for X1, X2, A, B being set
for F1 being SetSequence of X1
for F2 being SetSequence of X2
for F being SetSequence of [:X1,X2:] st F1 is non-descending & lim F1 = A & F2 is non-descending & lim F2 = B & ( for n being Nat holds F . n = [:(F1 . n),(F2 . n):] ) holds
lim F = [:A,B:]
proof end;

notation
let R be Relation;
let x be set ;
synonym X-section (R,x) for Im (R,x);
end;

notation
let R be Relation;
let y be set ;
synonym Y-section (R,y) for Coim (R,y);
end;

Lm1: now :: thesis: for X, Y, x being set
for E being Subset of [:X,Y:] holds X-section (E,x) = { y where y is Element of Y : [x,y] in E }
let X, Y, x be set ; :: thesis: for E being Subset of [:X,Y:] holds X-section (E,x) = { y where y is Element of Y : [x,y] in E }
let E be Subset of [:X,Y:]; :: thesis: X-section (E,x) = { y where y is Element of Y : [x,y] in E }
set A = { y where y is Element of Y : [x,y] in E } ;
thus X-section (E,x) = { y where y is Element of Y : [x,y] in E } :: thesis: verum
proof
thus X-section (E,x) c= { y where y is Element of Y : [x,y] in E } :: according to XBOOLE_0:def 10 :: thesis: { y where y is Element of Y : [x,y] in E } c= X-section (E,x)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X-section (E,x) or a in { y where y is Element of Y : [x,y] in E } )
assume a in X-section (E,x) ; :: thesis: a in { y where y is Element of Y : [x,y] in E }
then consider z being object such that
z in dom E and
A2: [z,a] in E and
A3: z in {x} by RELAT_1:110;
A4: z = x by A3, TARSKI:def 1;
a in rng E by A2, XTUPLE_0:def 13;
hence a in { y where y is Element of Y : [x,y] in E } by A2, A4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { y where y is Element of Y : [x,y] in E } or a in X-section (E,x) )
assume a in { y where y is Element of Y : [x,y] in E } ; :: thesis: a in X-section (E,x)
then consider y being Element of Y such that
A5: a = y and
A6: [x,y] in E ;
A7: x in dom E by A6, XTUPLE_0:def 12;
x in {x} by TARSKI:def 1;
hence a in X-section (E,x) by A5, A6, A7, RELAT_1:110; :: thesis: verum
end;
end;

Lm2: now :: thesis: for X, Y, y being set
for E being Subset of [:X,Y:] holds Y-section (E,y) = { x where x is Element of X : [x,y] in E }
let X, Y, y be set ; :: thesis: for E being Subset of [:X,Y:] holds Y-section (E,y) = { x where x is Element of X : [x,y] in E }
let E be Subset of [:X,Y:]; :: thesis: Y-section (E,y) = { x where x is Element of X : [x,y] in E }
set A = { x where x is Element of X : [x,y] in E } ;
thus Y-section (E,y) = { x where x is Element of X : [x,y] in E } :: thesis: verum
proof
thus Y-section (E,y) c= { x where x is Element of X : [x,y] in E } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of X : [x,y] in E } c= Y-section (E,y)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y-section (E,y) or a in { x where x is Element of X : [x,y] in E } )
assume a in Y-section (E,y) ; :: thesis: a in { x where x is Element of X : [x,y] in E }
then consider z being object such that
z in rng E and
A2: [a,z] in E and
A3: z in {y} by RELAT_1:131;
A4: z = y by A3, TARSKI:def 1;
a in dom E by A2, XTUPLE_0:def 12;
hence a in { x where x is Element of X : [x,y] in E } by A2, A4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { x where x is Element of X : [x,y] in E } or a in Y-section (E,y) )
assume a in { x where x is Element of X : [x,y] in E } ; :: thesis: a in Y-section (E,y)
then consider x being Element of X such that
A5: a = x and
A6: [x,y] in E ;
A7: y in rng E by A6, XTUPLE_0:def 13;
y in {y} by TARSKI:def 1;
hence a in Y-section (E,y) by A5, A6, A7, RELAT_1:131; :: thesis: verum
end;
end;

definition
let X, Y be set ;
let E be Subset of [:X,Y:];
let x be set ;
:: original: X-section
redefine func X-section (E,x) -> Subset of Y equals :: MEASUR11:def 4
 { y where y is Element of Y : [x,y] in E } ;
coherence
X-section (E,x) is Subset of Y
proof end;
compatibility
for b1 being Subset of Y holds
( b1 = X-section (E,x) iff b1 = { y where y is Element of Y : [x,y] in E } ) by Lm1;
end;

:: deftheorem defines X-section MEASUR11:def 4 :
for X, Y being set
for E being Subset of [:X,Y:]
for x being set holds X-section (E,x) = { y where y is Element of Y : [x,y] in E } ;

definition
let X, Y be set ;
let E be Subset of [:X,Y:];
let y be set ;
:: original: Y-section
redefine func Y-section (E,y) -> Subset of X equals :: MEASUR11:def 5
 { x where x is Element of X : [x,y] in E } ;
coherence
Y-section (E,y) is Subset of X
proof end;
compatibility
for b1 being Subset of X holds
( b1 = Y-section (E,y) iff b1 = { x where x is Element of X : [x,y] in E } ) by Lm2;
end;

:: deftheorem defines Y-section MEASUR11:def 5 :
for X, Y being set
for E being Subset of [:X,Y:]
for y being set holds Y-section (E,y) = { x where x is Element of X : [x,y] in E } ;

theorem Th14: :: MEASUR11:20
for X, Y, p being set
for E1, E2 being Subset of [:X,Y:] st E1 c= E2 holds
X-section (E1,p) c= X-section (E2,p) by RELAT_1:124;

theorem Th15: :: MEASUR11:21
for X, Y, p being set
for E1, E2 being Subset of [:X,Y:] st E1 c= E2 holds
Y-section (E1,p) c= Y-section (E2,p) by RELAT_1:144;

theorem Th16: :: MEASUR11:22
for X, Y being non empty set
for A being Subset of X
for B being Subset of Y
for p being set holds
( ( p in A implies X-section ([:A,B:],p) = B ) & ( not p in A implies X-section ([:A,B:],p) = {} ) & ( p in B implies Y-section ([:A,B:],p) = A ) & ( not p in B implies Y-section ([:A,B:],p) = {} ) )
proof end;

theorem Th17: :: MEASUR11:23
for X, Y being non empty set
for E being Subset of [:X,Y:]
for p being set holds
( ( not p in X implies X-section (E,p) = {} ) & ( not p in Y implies Y-section (E,p) = {} ) )
proof end;

theorem :: MEASUR11:24
for X, Y being non empty set
for p being set holds
( X-section (({} [:X,Y:]),p) = {} & Y-section (({} [:X,Y:]),p) = {} & ( p in X implies X-section (([#] [:X,Y:]),p) = Y ) & ( p in Y implies Y-section (([#] [:X,Y:]),p) = X ) )
proof end;

theorem Th19: :: MEASUR11:25
for X, Y being non empty set
for E being Subset of [:X,Y:]
for p being set holds
( ( p in X implies X-section (([:X,Y:] \ E),p) = Y \ (X-section (E,p)) ) & ( p in Y implies Y-section (([:X,Y:] \ E),p) = X \ (Y-section (E,p)) ) )
proof end;

theorem Th20: :: MEASUR11:26
for X, Y being non empty set
for E1, E2 being Subset of [:X,Y:]
for p being set holds
( X-section ((E1 \/ E2),p) = (X-section (E1,p)) \/ (X-section (E2,p)) & Y-section ((E1 \/ E2),p) = (Y-section (E1,p)) \/ (Y-section (E2,p)) )
proof end;

theorem Th21: :: MEASUR11:27
for X, Y being non empty set
for E1, E2 being Subset of [:X,Y:]
for p being set holds
( X-section ((E1 /\ E2),p) = (X-section (E1,p)) /\ (X-section (E2,p)) & Y-section ((E1 /\ E2),p) = (Y-section (E1,p)) /\ (Y-section (E2,p)) )
proof end;

theorem Th22: :: MEASUR11:28
for X being set
for Y being non empty set
for F being FinSequence of bool [:X,Y:]
for Fy being FinSequence of bool Y
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
proof end;

theorem Th23: :: MEASUR11:29
for X being non empty set
for Y being set
for F being FinSequence of bool [:X,Y:]
for Fx being FinSequence of bool X
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)
proof end;

theorem Th24: :: MEASUR11:30
for X being set
for Y being non empty set
for p being set
for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((union (rng F)),p) = union (rng Fy)
proof end;

theorem Th25: :: MEASUR11:31
for X being set
for Y being non empty set
for p being set
for F being SetSequence of [:X,Y:]
for Fy being SetSequence of Y st ( for n being Nat holds Fy . n = X-section ((F . n),p) ) holds
X-section ((meet (rng F)),p) = meet (rng Fy)
proof end;

theorem Th26: :: MEASUR11:32
for X being non empty set
for Y, p being set
for F being SetSequence of [:X,Y:]
for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)
proof end;

theorem Th27: :: MEASUR11:33
for X being non empty set
for Y, p being set
for F being SetSequence of [:X,Y:]
for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((meet (rng F)),p) = meet (rng Fx)
proof end;

theorem Th28: :: MEASUR11:34
for X, Y being non empty set
for x, y being set
for E being Subset of [:X,Y:] holds
( (chi (E,[:X,Y:])) . (x,y) = (chi ((X-section (E,x)),Y)) . y & (chi (E,[:X,Y:])) . (x,y) = (chi ((Y-section (E,y)),X)) . x )
proof end;

theorem Th29: :: MEASUR11:35
for X, Y being non empty set
for E1, E2 being Subset of [:X,Y:]
for p being set st E1 misses E2 holds
( X-section (E1,p) misses X-section (E2,p) & Y-section (E1,p) misses Y-section (E2,p) )
proof end;

theorem :: MEASUR11:36
for X, Y being non empty set
for F being disjoint_valued FinSequence of bool [:X,Y:]
for p being set holds
( ex Fy being disjoint_valued FinSequence of bool X st
( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Y-section ((F . n),p) ) ) & ex Fx being disjoint_valued FinSequence of bool Y st
( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = X-section ((F . n),p) ) ) )
proof end;

theorem :: MEASUR11:37
for X, Y being non empty set
for F being V55() SetSequence of [:X,Y:]
for p being set holds
( ex Fy being V55() SetSequence of X st
for n being Nat holds Fy . n = Y-section ((F . n),p) & ex Fx being V55() SetSequence of Y st
for n being Nat holds Fx . n = X-section ((F . n),p) )
proof end;

theorem :: MEASUR11:38
for X, Y being non empty set
for x, y being set
for E1, E2 being Subset of [:X,Y:] st E1 misses E2 holds
( (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((X-section (E1,x)),Y)) . y) + ((chi ((X-section (E2,x)),Y)) . y) & (chi ((E1 \/ E2),[:X,Y:])) . (x,y) = ((chi ((Y-section (E1,y)),X)) . x) + ((chi ((Y-section (E2,y)),X)) . x) )
proof end;

theorem Th33: :: MEASUR11:39
for X being set
for Y being non empty set
for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending
proof end;

theorem Th34: :: MEASUR11:40
for X being non empty set
for Y, x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-descending
proof end;

theorem Th35: :: MEASUR11:41
for X being set
for Y being non empty set
for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-ascending
proof end;

theorem Th36: :: MEASUR11:42
for X being non empty set
for Y, x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-ascending
proof end;

theorem Th37: :: MEASUR11:43
for X being set
for Y being non empty set
for E being SetSequence of [:X,Y:]
for x being set st E is non-descending holds
ex G being SetSequence of Y st
( G is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
proof end;

theorem Th38: :: MEASUR11:44
for X being non empty set
for Y being set
for E being SetSequence of [:X,Y:]
for x being set st E is non-descending holds
ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
proof end;

theorem Th39: :: MEASUR11:45
for X being set
for Y being non empty set
for E being SetSequence of [:X,Y:]
for x being set st E is non-ascending holds
ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
proof end;

theorem Th40: :: MEASUR11:46
for X being non empty set
for Y being set
for E being SetSequence of [:X,Y:]
for x being set st E is non-ascending holds
ex G being SetSequence of X st
( G is non-ascending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
proof end;

theorem Th42: :: MEASUR11:47
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 K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds X-section (C,p) in S2 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
proof end;

theorem Th43: :: MEASUR11:48
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 K being set st K = { C where C is Subset of [:X1,X2:] : for p being set holds Y-section (C,p) in S1 } holds
( Field_generated_by (measurable_rectangles (S1,S2)) c= K & K is SigmaField of [:X1,X2:] )
proof end;

theorem Th44: :: MEASUR11:49
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)) holds
( ( for p being set holds X-section (E,p) in S2 ) & ( for p being set holds Y-section (E,p) in S1 ) )
proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let E be Element of sigma (measurable_rectangles (S1,S2));
let x be set ;
func Measurable-X-section (E,x) -> Element of S2 equals :: MEASUR11:def 6
 X-section (E,x);
correctness
coherence
X-section (E,x) is Element of S2;
by Th44;
end;

:: deftheorem defines Measurable-X-section MEASUR11:def 6 :
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 set holds Measurable-X-section (E,x) = X-section (E,x);

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let E be Element of sigma (measurable_rectangles (S1,S2));
let y be set ;
func Measurable-Y-section (E,y) -> Element of S1 equals :: MEASUR11:def 7
 Y-section (E,y);
correctness
coherence
Y-section (E,y) is Element of S1;
by Th44;
end;

:: deftheorem defines Measurable-Y-section MEASUR11:def 7 :
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 y being set holds Measurable-Y-section (E,y) = Y-section (E,y);

theorem :: MEASUR11:50
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
proof end;

theorem :: MEASUR11:51
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
proof end;

theorem Th47: :: MEASUR11: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 A being Element of S1
for B being Element of S2
for x being Element of X1 holds (M2 . B) * ((chi (A,X1)) . x) = Integral (M2,(ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x)))
proof end;

theorem Th48: :: MEASUR11:53
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))
for A being Element of S1
for B being Element of S2
for x being Element of X1 st E = [:A,B:] holds
M2 . (Measurable-X-section (E,x)) = (M2 . B) * ((chi (A,X1)) . x)
proof end;

theorem Th49: :: MEASUR11:54
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 A being Element of S1
for B being Element of S2
for y being Element of X2 holds (M1 . A) * ((chi (B,X2)) . y) = Integral (M1,(ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y)))
proof end;

theorem Th50: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2
for y being Element of X2 st E = [:A,B:] holds
M1 . (Measurable-Y-section (E,y)) = (M1 . A) * ((chi (B,X2)) . y)
proof end;

definition
let X, Y be non empty set ;
let G be FUNCTION_DOMAIN of X,Y;
let F be FinSequence of G;
let n be Nat;
:: original: /.
redefine func F /. n -> Element of G;
correctness
coherence
F /. n is Element of G;
;
end;

definition
let X be set ;
let F be FinSequence of Funcs (X,ExtREAL);
attr F is without_+infty-valued means :DEF10: :: MEASUR11:def 8
 for n being Nat st n in dom F holds
F . n is without+infty ;
attr F is without_-infty-valued means :DEF11: :: MEASUR11:def 9
 for n being Nat st n in dom F holds
F . n is without-infty ;
end;

:: deftheorem DEF10 defines without_+infty-valued MEASUR11:def 8 :
for X being set
for F being FinSequence of Funcs (X,ExtREAL) holds
( F is without_+infty-valued iff for n being Nat st n in dom F holds
F . n is without+infty );

:: deftheorem DEF11 defines without_-infty-valued MEASUR11:def 9 :
for X being set
for F being FinSequence of Funcs (X,ExtREAL) holds
( F is without_-infty-valued iff for n being Nat st n in dom F holds
F . n is without-infty );

theorem Th52: :: MEASUR11:56
for X being non empty set holds
( <*(X --> 0)*> is FinSequence of Funcs (X,ExtREAL) & ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without+infty ) & ( for n being Nat st n in dom <*(X --> 0)*> holds
<*(X --> 0)*> . n is without-infty ) )
proof end;

registration
let X be non empty set ;
cluster Relation-like NAT -defined Funcs (X,ExtREAL) -valued Function-like V38() FinSequence-like FinSubsequence-like without_+infty-valued without_-infty-valued for FinSequence of Funcs (X,ExtREAL);
existence
ex b1 being FinSequence of Funcs (X,ExtREAL) st
( b1 is without_+infty-valued & b1 is without_-infty-valued )
proof end;
end;

theorem Th53: :: MEASUR11:57
for X being non empty set
for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL)
for n being Nat st n in dom F holds
(F /. n) " {+infty} = {}
proof end;

theorem Th54: :: MEASUR11:58
for X being non empty set
for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL)
for n being Nat st n in dom F holds
(F /. n) " {-infty} = {}
proof end;

theorem :: MEASUR11:59
for X being non empty set
for F being FinSequence of Funcs (X,ExtREAL) st ( F is without_+infty-valued or F is without_-infty-valued ) holds
for n, m being Nat st n in dom F & m in dom F holds
dom ((F /. n) + (F /. m)) = X
proof end;

definition
let X be non empty set ;
let F be FinSequence of Funcs (X,ExtREAL);
attr F is summable means :DEF12: :: MEASUR11:def 10
( F is without_+infty-valued or F is without_-infty-valued );
end;

:: deftheorem DEF12 defines summable MEASUR11:def 10 :
for X being non empty set
for F being FinSequence of Funcs (X,ExtREAL) holds
( F is summable iff ( F is without_+infty-valued or F is without_-infty-valued ) );

registration
let X be non empty set ;
cluster Relation-like NAT -defined Funcs (X,ExtREAL) -valued Function-like V38() FinSequence-like FinSubsequence-like summable for FinSequence of Funcs (X,ExtREAL);
existence
ex b1 being FinSequence of Funcs (X,ExtREAL) st b1 is summable
proof end;
end;

definition
let X be non empty set ;
let F be summable FinSequence of Funcs (X,ExtREAL);
func Partial_Sums F -> FinSequence of Funcs (X,ExtREAL) means :DEF13: :: MEASUR11:def 11
( len F = len it & F . 1 = it . 1 & ( for n being Nat st 1 <= n & n < len F holds
it . (n + 1) = (it /. n) + (F /. (n + 1)) ) );
existence
ex b1 being FinSequence of Funcs (X,ExtREAL) st
( len F = len b1 & F . 1 = b1 . 1 & ( for n being Nat st 1 <= n & n < len F holds
b1 . (n + 1) = (b1 /. n) + (F /. (n + 1)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of Funcs (X,ExtREAL) st len F = len b1 & F . 1 = b1 . 1 & ( for n being Nat st 1 <= n & n < len F holds
b1 . (n + 1) = (b1 /. n) + (F /. (n + 1)) ) & len F = len b2 & F . 1 = b2 . 1 & ( for n being Nat st 1 <= n & n < len F holds
b2 . (n + 1) = (b2 /. n) + (F /. (n + 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem DEF13 defines Partial_Sums MEASUR11:def 11 :
for X being non empty set
for F being summable FinSequence of Funcs (X,ExtREAL)
for b3 being FinSequence of Funcs (X,ExtREAL) holds
( b3 = Partial_Sums F iff ( len F = len b3 & F . 1 = b3 . 1 & ( for n being Nat st 1 <= n & n < len F holds
b3 . (n + 1) = (b3 /. n) + (F /. (n + 1)) ) ) );

registration
let X be non empty set ;
cluster without_+infty-valued -> summable for FinSequence of Funcs (X,ExtREAL);
correctness
coherence
for b1 being FinSequence of Funcs (X,ExtREAL) st b1 is without_+infty-valued holds
b1 is summable ;
;
cluster without_-infty-valued -> summable for FinSequence of Funcs (X,ExtREAL);
correctness
coherence
for b1 being FinSequence of Funcs (X,ExtREAL) st b1 is without_-infty-valued holds
b1 is summable ;
;
end;

theorem Th56: :: MEASUR11:60
for X being non empty set
for F being without_+infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_+infty-valued
proof end;

theorem Th57: :: MEASUR11:61
for X being non empty set
for F being without_-infty-valued FinSequence of Funcs (X,ExtREAL) holds Partial_Sums F is without_-infty-valued
proof end;

theorem :: MEASUR11:62
for X being non empty set
for A being set
for er being ExtReal
for f being Function of X,ExtREAL st ( for x being Element of X holds f . x = er * ((chi (A,X)) . x) ) holds
( ( er = +infty implies f = Xchi (A,X) ) & ( er = -infty implies f = - (Xchi (A,X)) ) & ( er <> +infty & er <> -infty implies ex r being Real st
( r = er & f = r (#) (chi (A,X)) ) ) )
proof end;

theorem Th59: :: MEASUR11:63
for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & A c= dom f holds
- f is A -measurable
proof end;

registration
let X be non empty set ;
let f be V175() PartFunc of X,ExtREAL;
cluster - f -> V176() ;
correctness
coherence
- f is without+infty ;
proof end;
end;

registration
let X be non empty set ;
let f be V176() PartFunc of X,ExtREAL;
cluster - f -> V175() ;
correctness
coherence
- f is without-infty ;
proof end;
end;

definition
let X be non empty set ;
let f1, f2 be V176() PartFunc of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V176() PartFunc of X,ExtREAL;
correctness
coherence
f1 + f2 is V176() PartFunc of X,ExtREAL;
by MESFUNC9:4;
end;

definition
let X be non empty set ;
let f1, f2 be V175() PartFunc of X,ExtREAL;
:: original: +
redefine func f1 + f2 -> V175() PartFunc of X,ExtREAL;
correctness
coherence
f1 + f2 is V175() PartFunc of X,ExtREAL;
by MESFUNC9:3;
end;

definition
let X be non empty set ;
let f1 be V176() PartFunc of X,ExtREAL;
let f2 be V175() PartFunc of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V176() PartFunc of X,ExtREAL;
correctness
coherence
f1 - f2 is V176() PartFunc of X,ExtREAL;
by MESFUNC9:6;
end;

definition
let X be non empty set ;
let f1 be V175() PartFunc of X,ExtREAL;
let f2 be V176() PartFunc of X,ExtREAL;
:: original: -
redefine func f1 - f2 -> V175() PartFunc of X,ExtREAL;
correctness
coherence
f1 - f2 is V175() PartFunc of X,ExtREAL;
by MESFUNC9:5;
end;

LEM10: for X being non empty set
for f being PartFunc of X,ExtREAL holds
( f " {+infty} = (- f) " {-infty} & f " {-infty} = (- f) " {+infty} )
proof end;

theorem Th60: :: MEASUR11:64
for X being non empty set
for f, g being PartFunc of X,ExtREAL holds
( - (f + g) = (- f) + (- g) & - (f - g) = (- f) + g & - (f - g) = g - f & - ((- f) + g) = f - g & - ((- f) + g) = f + (- g) )
proof end;

theorem Th61: :: MEASUR11:65
for X being non empty set
for S being SigmaField of X
for f, g being V176() PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & g is A -measurable & A c= dom (f + g) holds
f + g is A -measurable
proof end;

theorem :: MEASUR11:66
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being V176() PartFunc of X,ExtREAL
for g being V175() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
proof end;

theorem :: MEASUR11:67
for X being non empty set
for S being SigmaField of X
for A being Element of S
for f being V175() PartFunc of X,ExtREAL
for g being V176() PartFunc of X,ExtREAL st f is A -measurable & g is A -measurable & A c= dom (f - g) holds
f - g is A -measurable
proof end;

theorem Th64: :: MEASUR11:68
for X being non empty set
for S being SigmaField of X
for P being Element of S
for F being summable FinSequence of Funcs (X,ExtREAL) st ( for n being Nat st n in dom F holds
F /. n is P -measurable ) holds
for n being Nat st n in dom F holds
(Partial_Sums F) /. n is P -measurable
proof end;

theorem Th65: :: MEASUR11:69
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 A being Element of S1
for B being Element of S2
for x being Element of X1
for y being Element of X2 st E = [:A,B:] holds
( Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) = (M2 . (Measurable-X-section (E,x))) * ((chi (A,X1)) . x) & Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) = (M1 . (Measurable-Y-section (E,y))) * ((chi (B,X2)) . y) )
proof end;

theorem Th66: :: MEASUR11:70
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)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 st
( len f = len A & len f = len B & E = Union f & ( for n being Nat st n in dom f holds
( proj1 (f . n) = A . n & proj2 (f . n) = B . n ) ) & ( for n being Nat
for x, y being set st n in dom f & x in X1 & y in X2 holds
(chi ((f . n),[:X1,X2:])) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) )
proof end;

theorem Th67: :: MEASUR11:71
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 x being Element of X1
for y being Element of X2
for U being Element of S1
for V being Element of S2 holds
( M1 . ((Measurable-Y-section (E,y)) /\ U) = Integral (M1,(ProjMap2 ((chi ((E /\ [:U,X2:]),[:X1,X2:])),y))) & M2 . ((Measurable-X-section (E,x)) /\ V) = Integral (M2,(ProjMap1 ((chi ((E /\ [:X1,V:]),[:X1,X2:])),x))) )
proof end;

theorem Th68: :: MEASUR11: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 being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1
for y being Element of X2 holds
( M1 . (Measurable-Y-section (E,y)) = Integral (M1,(ProjMap2 ((chi (E,[:X1,X2:])),y))) & M2 . (Measurable-X-section (E,x)) = Integral (M2,(ProjMap1 ((chi (E,[:X1,X2:])),x))) )
proof end;

theorem :: MEASUR11:73
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 disjoint_valued FinSequence of measurable_rectangles (S1,S2)
for x being Element of X1
for n being Nat
for En being Element of sigma (measurable_rectangles (S1,S2))
for An being Element of S1
for Bn being Element of S2 st n in dom f & f . n = En & En = [:An,Bn:] holds
Integral (M2,(ProjMap1 ((chi ((f . n),[:X1,X2:])),x))) = (M2 . (Measurable-X-section (En,x))) * ((chi (An,X1)) . x) by Th65;

theorem Th70: :: MEASUR11:74
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)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds
ex f being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex Xf being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) st
( E = Union f & len f in dom f & len f = len A & len f = len B & len f = len Xf & ( for n being Nat st n in dom f holds
f . n = [:(A . n),(B . n):] ) & ( for n being Nat st n in dom Xf holds
Xf . n = chi ((f . n),[:X1,X2:]) ) & (Partial_Sums Xf) . (len Xf) = chi (E,[:X1,X2:]) & ( for n being Nat
for x, y being set st n in dom Xf & x in X1 & y in X2 holds
(Xf . n) . (x,y) = ((chi ((A . n),X1)) . x) * ((chi ((B . n),X2)) . y) ) & ( for x being Element of X1 holds ProjMap1 ((chi (E,[:X1,X2:])),x) = ProjMap1 (((Partial_Sums Xf) /. (len Xf)),x) ) & ( for y being Element of X2 holds ProjMap2 ((chi (E,[:X1,X2:])),y) = ProjMap2 (((Partial_Sums Xf) /. (len Xf)),y) ) )
proof end;

theorem Th71: :: MEASUR11:75
for X1, X2 being non empty set
for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))
proof end;

theorem Th75: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) & E <> {} holds
ex F being disjoint_valued FinSequence of measurable_rectangles (S1,S2) ex A being FinSequence of S1 ex B being FinSequence of S2 ex C being summable FinSequence of Funcs ([:X1,X2:],ExtREAL) ex I being summable FinSequence of Funcs (X1,ExtREAL) ex J being summable FinSequence of Funcs (X2,ExtREAL) st
( E = Union F & len F in dom F & len F = len A & len F = len B & len F = len C & len F = len I & len F = len J & ( for n being Nat st n in dom C holds
C . n = chi ((F . n),[:X1,X2:]) ) & (Partial_Sums C) /. (len C) = chi (E,[:X1,X2:]) & ( for x being Element of X1
for n being Nat st n in dom I holds
(I . n) . x = Integral (M2,(ProjMap1 ((C /. n),x))) ) & ( for n being Nat
for P being Element of S1 st n in dom I holds
I /. n is P -measurable ) & ( for x being Element of X1 holds Integral (M2,(ProjMap1 (((Partial_Sums C) /. (len C)),x))) = ((Partial_Sums I) /. (len I)) . x ) & ( for y being Element of X2
for n being Nat st n in dom J holds
(J . n) . y = Integral (M1,(ProjMap2 ((C /. n),y))) ) & ( for n being Nat
for P being Element of S2 st n in dom J holds
J /. n is P -measurable ) & ( for y being Element of X2 holds Integral (M1,(ProjMap2 (((Partial_Sums C) /. (len C)),y))) = ((Partial_Sums J) /. (len J)) . y ) )
proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let F be Set_Sequence of sigma (measurable_rectangles (S1,S2));
let n be Nat;
:: original: .
redefine func F . n -> Element of sigma (measurable_rectangles (S1,S2));
coherence
F . n is Element of sigma (measurable_rectangles (S1,S2)) by MEASURE8:def 2;
end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let F be Function of [:NAT,(sigma (measurable_rectangles (S1,S2))):],(sigma (measurable_rectangles (S1,S2)));
let n be Element of NAT ;
let E be Element of sigma (measurable_rectangles (S1,S2));
:: original: .
redefine func F . (n,E) -> Element of sigma (measurable_rectangles (S1,S2));
coherence
F . (n,E) is Element of sigma (measurable_rectangles (S1,S2))
proof end;
end;

theorem Th76: :: MEASUR11: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))
for V being Element of S2 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ V) ) & ( for P being Element of S1 holds F is P -measurable ) )
proof end;

theorem Th77: :: MEASUR11: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 V being Element of S1 st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ V) ) & ( for P being Element of S2 holds F is P -measurable ) )
proof end;

theorem Th78: :: MEASUR11:79
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 E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for B being Element of S2 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
proof end;

theorem Th79: :: MEASUR11: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 E being Element of sigma (measurable_rectangles (S1,S2)) st E in Field_generated_by (measurable_rectangles (S1,S2)) holds
for B being Element of S1 holds E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for x being Element of X2 holds F . x = M1 . ((Measurable-Y-section (E,x)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }
proof end;

theorem Th80: :: MEASUR11:81
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 B being Element of S2 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
proof end;

theorem Th81: :: MEASUR11: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 B being Element of S1 holds Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let M be sigma_Measure of S;
attr M is sigma_finite means :: MEASUR11:def 12
 ex E being Set_Sequence of S st
( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X );
end;

:: deftheorem defines sigma_finite MEASUR11:def 12 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( M is sigma_finite iff ex E being Set_Sequence of S st
( ( for n being Nat holds M . (E . n) < +infty ) & Union E = X ) );

LM0902a: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st M is sigma_finite holds
ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X )
proof end;

LM0902b: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S st ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) holds
M is sigma_finite
proof end;

theorem :: MEASUR11:83
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds
( M is sigma_finite iff ex F being Set_Sequence of S st
( F is non-descending & ( for n being Nat holds M . (F . n) < +infty ) & lim F = X ) ) by LM0902a, LM0902b;

theorem :: MEASUR11:84
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds M = (C_Meas M) | (Field_generated_by S)
proof end;

theorem Th84: :: MEASUR11:85
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 B being Element of S2 st M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
proof end;

theorem Th85: :: MEASUR11:86
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 B being Element of S1 st M1 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) } is MonotoneClass of [:X1,X2:]
proof end;

theorem :: MEASUR11:87
for X being non empty set
for F being Field_Subset of X
for L being SetSequence of X st rng L is MonotoneClass of X & F c= rng L holds
( sigma F = monotoneclass F & sigma F c= rng L )
proof end;

theorem Th87: :: MEASUR11:88
for X being non empty set
for F being Field_Subset of X
for K being Subset-Family of X st K is MonotoneClass of X & F c= K holds
( sigma F = monotoneclass F & sigma F c= K )
proof end;

theorem Th88: :: MEASUR11:89
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 B being Element of S2 st M2 . B < +infty holds
sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . ((Measurable-X-section (E,x)) /\ B) ) & ( for V being Element of S1 holds F is V -measurable ) ) }
proof end;

theorem Th89: :: MEASUR11:90
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 B being Element of S1 st M1 . B < +infty holds
sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . ((Measurable-Y-section (E,y)) /\ B) ) & ( for V being Element of S2 holds F is V -measurable ) ) }
proof end;

theorem Th90: :: MEASUR11:91
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
ex F being Function of X1,ExtREAL st
( ( for x being Element of X1 holds F . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds F is V -measurable ) )
proof end;

theorem Th91: :: MEASUR11:92
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
ex F being Function of X2,ExtREAL st
( ( for y being Element of X2 holds F . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds F is V -measurable ) )
proof end;

definition
let X1, X2 be non empty set ;
let S1 be SigmaField of X1;
let S2 be SigmaField of X2;
let M2 be sigma_Measure of S2;
let E be Element of sigma (measurable_rectangles (S1,S2));
assume A1: M2 is sigma_finite ;
func Y-vol (E,M2) -> V102() Function of X1,ExtREAL means :DefYvol: :: MEASUR11:def 13
( ( for x being Element of X1 holds it . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds it is V -measurable ) );
existence
ex b1 being V102() Function of X1,ExtREAL st
( ( for x being Element of X1 holds b1 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b1 is V -measurable ) )
proof end;
uniqueness
for b1, b2 being V102() Function of X1,ExtREAL st ( for x being Element of X1 holds b1 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b1 is V -measurable ) & ( for x being Element of X1 holds b2 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b2 is V -measurable ) holds
b1 = b2
proof end;
end;

:: deftheorem DefYvol defines Y-vol MEASUR11:def 13 :
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
for b7 being V102() Function of X1,ExtREAL holds
( b7 = Y-vol (E,M2) iff ( ( for x being Element of X1 holds b7 . x = M2 . (Measurable-X-section (E,x)) ) & ( for V being Element of S1 holds b7 is V -measurable ) ) );

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 E be Element of sigma (measurable_rectangles (S1,S2));
assume A1: M1 is sigma_finite ;
func X-vol (E,M1) -> V102() Function of X2,ExtREAL means :DefXvol: :: MEASUR11:def 14
( ( for y being Element of X2 holds it . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds it is V -measurable ) );
existence
ex b1 being V102() Function of X2,ExtREAL st
( ( for y being Element of X2 holds b1 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b1 is V -measurable ) )
proof end;
uniqueness
for b1, b2 being V102() Function of X2,ExtREAL st ( for y being Element of X2 holds b1 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b1 is V -measurable ) & ( for y being Element of X2 holds b2 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b2 is V -measurable ) holds
b1 = b2
proof end;
end;

:: deftheorem DefXvol defines X-vol MEASUR11:def 14 :
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
for b7 being V102() Function of X2,ExtREAL holds
( b7 = X-vol (E,M1) iff ( ( for y being Element of X2 holds b7 . y = M1 . (Measurable-Y-section (E,y)) ) & ( for V being Element of S2 holds b7 is V -measurable ) ) );

theorem Th92: :: MEASUR11:93
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Y-vol ((E1 \/ E2),M2) = (Y-vol (E1,M2)) + (Y-vol (E2,M2))
proof end;

theorem Th93: :: MEASUR11:94
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
X-vol ((E1 \/ E2),M1) = (X-vol (E1,M1)) + (X-vol (E2,M1))
proof end;

theorem Th94: :: MEASUR11:95
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M2 is sigma_finite & E1 misses E2 holds
Integral (M1,(Y-vol ((E1 \/ E2),M2))) = (Integral (M1,(Y-vol (E1,M2)))) + (Integral (M1,(Y-vol (E2,M2))))
proof end;

theorem Th95: :: MEASUR11:96
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 E1, E2 being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & E1 misses E2 holds
Integral (M2,(X-vol ((E1 \/ E2),M1))) = (Integral (M2,(X-vol (E1,M1)))) + (Integral (M2,(X-vol (E2,M1))))
proof end;

theorem Th96: :: MEASUR11:97
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 A being Element of S1
for B being Element of S2 st E = [:A,B:] & M2 is sigma_finite holds
( ( M2 . B = +infty implies Y-vol (E,M2) = Xchi (A,X1) ) & ( M2 . B <> +infty implies ex r being Real st
( r = M2 . B & Y-vol (E,M2) = r (#) (chi (A,X1)) ) ) )
proof end;

theorem Th97: :: MEASUR11:98
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 A being Element of S1
for B being Element of S2 st E = [:A,B:] & M1 is sigma_finite holds
( ( M1 . A = +infty implies X-vol (E,M1) = Xchi (B,X2) ) & ( M1 . A <> +infty implies ex r being Real st
( r = M1 . A & X-vol (E,M1) = r (#) (chi (B,X2)) ) ) )
proof end;

theorem Th98: :: MEASUR11:99
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for A being Element of S
for r being Real st r >= 0 holds
Integral (M,(r (#) (chi (A,X)))) = r * (M . A)
proof end;

theorem Th99: :: MEASUR11:100
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 FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
proof end;

theorem Th100: :: MEASUR11:101
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 FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
proof end;

theorem Th102: :: MEASUR11:102
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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M1,(Y-vol ((Union F),M2)))
proof end;

theorem Th103: :: MEASUR11:103
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 disjoint_valued FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
proof end;

theorem Th104: :: MEASUR11:104
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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M2 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th105: :: MEASUR11:105
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 E in Field_generated_by (measurable_rectangles (S1,S2)) & M1 is sigma_finite holds
for V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st V = [:A,B:] holds
E in { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th106: :: MEASUR11:106
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] holds
Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th107: :: MEASUR11:107
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] holds
Field_generated_by (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th108: :: MEASUR11:108
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, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-descending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
proof end;

theorem Th109: :: MEASUR11:109
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, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-descending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-descending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
proof end;

theorem Th110: :: MEASUR11:110
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, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for x being Element of X1 st P is non-ascending & lim P = E holds
ex K being SetSequence of S2 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-X-section ((P . n),x)) /\ (Measurable-X-section (V,x)) ) & lim K = (Measurable-X-section (E,x)) /\ (Measurable-X-section (V,x)) )
proof end;

theorem Th111: :: MEASUR11:111
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, V being Element of sigma (measurable_rectangles (S1,S2))
for P being Set_Sequence of sigma (measurable_rectangles (S1,S2))
for y being Element of X2 st P is non-ascending & lim P = E holds
ex K being SetSequence of S1 st
( K is non-ascending & ( for n being Nat holds K . n = (Measurable-Y-section ((P . n),y)) /\ (Measurable-Y-section (V,y)) ) & lim K = (Measurable-Y-section (E,y)) /\ (Measurable-Y-section (V,y)) )
proof end;

theorem Th112: :: MEASUR11:112
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
proof end;

theorem Th113: :: MEASUR11:113
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
{ E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) } is MonotoneClass of [:X1,X2:]
proof end;

theorem Th114: :: MEASUR11:114
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M2 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M2 . B < +infty holds
sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M1,(Y-vol ((E /\ V),M2))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th115: :: MEASUR11:115
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 V being Element of sigma (measurable_rectangles (S1,S2))
for A being Element of S1
for B being Element of S2 st M1 is sigma_finite & V = [:A,B:] & (product_sigma_Measure (M1,M2)) . V < +infty & M1 . A < +infty holds
sigma (measurable_rectangles (S1,S2)) c= { E where E is Element of sigma (measurable_rectangles (S1,S2)) : Integral (M2,(X-vol ((E /\ V),M1))) = (product_sigma_Measure (M1,M2)) . (E /\ V) }
proof end;

theorem Th116: :: MEASUR11:116
for X, Y being set
for A being SetSequence of X
for B being SetSequence of Y
for C being SetSequence of [:X,Y:] st A is non-descending & B is non-descending & ( for n being Nat holds C . n = [:(A . n),(B . n):] ) holds
( C is non-descending & C is convergent & Union C = [:(Union A),(Union B):] )
proof end;

:: WP: Fubini's theorem
theorem :: MEASUR11:117
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))) = (product_sigma_Measure (M1,M2)) . E
proof end;

:: WP: Fubini's theorem
theorem :: MEASUR11:118
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 (M2,(X-vol (E,M1))) = (product_sigma_Measure (M1,M2)) . E
proof end;