:: Multidimensional Measure Space and Integration
:: by Noboru Endou and Yasunari Shidama
::
:: Received November 21, 2023
:: Copyright (c) 2023-2024 Association of Mizar Users


definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
assume A1: n <= m ;
func ElmFin (X,n) -> non empty set equals :Def1: :: MEASUR13:def 1
X . n;
correctness
coherence
X . n is non empty set ;
proof end;
end;

:: deftheorem Def1 defines ElmFin MEASUR13:def 1 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n <= m holds
ElmFin (X,n) = X . n;

definition
let m be Nat;
let X be non-empty m -element FinSequence;
mode sigmaFieldFamily of X -> m -element FinSequence means :Def2: :: MEASUR13:def 2
 for i being Nat st i in Seg m holds
it . i is SigmaField of (X . i);
existence
ex b1 being m -element FinSequence st
for i being Nat st i in Seg m holds
b1 . i is SigmaField of (X . i)
proof end;
end;

:: deftheorem Def2 defines sigmaFieldFamily MEASUR13:def 2 :
for m being Nat
for X being non-empty b1 -element FinSequence
for b3 being b1 -element FinSequence holds
( b3 is sigmaFieldFamily of X iff for i being Nat st i in Seg m holds
b3 . i is SigmaField of (X . i) );

theorem :: MEASUR13:1
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
S . n is SigmaField of (ElmFin (X,n))
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
func ProdFinSeq X -> non-empty m -element FinSequence means :Def3: :: MEASUR13:def 3
( it . 1 = X . 1 & ( for i being non zero Nat st i < m holds
it . (i + 1) = [:(it . i),(X . (i + 1)):] ) );
existence
ex b1 being non-empty m -element FinSequence st
( b1 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
b1 . (i + 1) = [:(b1 . i),(X . (i + 1)):] ) )
proof end;
uniqueness
for b1, b2 being non-empty m -element FinSequence st b1 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
b1 . (i + 1) = [:(b1 . i),(X . (i + 1)):] ) & b2 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
b2 . (i + 1) = [:(b2 . i),(X . (i + 1)):] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ProdFinSeq MEASUR13:def 3 :
for m being non zero Nat
for X, b3 being non-empty b1 -element FinSequence holds
( b3 = ProdFinSeq X iff ( b3 . 1 = X . 1 & ( for i being non zero Nat st i < m holds
b3 . (i + 1) = [:(b3 . i),(X . (i + 1)):] ) ) );

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
func CarProduct X -> set equals :: MEASUR13:def 4
(ProdFinSeq X) . m;
correctness
coherence
(ProdFinSeq X) . m is set ;
;
end;

:: deftheorem defines CarProduct MEASUR13:def 4 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence holds CarProduct X = (ProdFinSeq X) . m;

registration
let m be non zero Nat;
let X be non-empty m -element FinSequence;
cluster CarProduct X -> non empty ;
coherence
not CarProduct X is empty
proof end;
end;

theorem Th2: :: MEASUR13:2
for m being non zero Nat
for k being Nat
for X being non-empty b1 -element FinSequence st k <= m holds
X | k is non-empty b2 -element FinSequence
proof end;

definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
assume A1: n <= m ;
func SubFin (X,n) -> non-empty n -element FinSequence equals :Def5: :: MEASUR13:def 5
X | n;
correctness
coherence
X | n is non-empty n -element FinSequence;
by A1, Th2;
end;

:: deftheorem Def5 defines SubFin MEASUR13:def 5 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n <= m holds
SubFin (X,n) = X | n;

definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
assume A1: n <= m ;
func SubFin (S,n) -> sigmaFieldFamily of SubFin (X,n) equals :Def6: :: MEASUR13:def 6
S | n;
correctness
coherence
S | n is sigmaFieldFamily of SubFin (X,n);
proof end;
end;

:: deftheorem Def6 defines SubFin MEASUR13:def 6 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
SubFin (S,n) = S | n;

definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
assume A1: n <= m ;
func ElmFin (S,n) -> SigmaField of (ElmFin (X,n)) equals :Def7: :: MEASUR13:def 7
S . n;
correctness
coherence
S . n is SigmaField of (ElmFin (X,n));
proof end;
end;

:: deftheorem Def7 defines ElmFin MEASUR13:def 7 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
ElmFin (S,n) = S . n;

Lm1: for n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X holds S is SemialgebraFamily of X
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
:: original: sigmaFieldFamily
redefine mode sigmaFieldFamily of X -> SemialgebraFamily of X;
correctness
coherence
for b1 being sigmaFieldFamily of X holds b1 is SemialgebraFamily of X;
by Lm1;
end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
mode sigmaMeasureFamily of S -> m -element FinSequence means :Def8: :: MEASUR13:def 8
 for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & it . i is sigma_Measure of Si );
existence
ex b1 being m -element FinSequence st
for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & b1 . i is sigma_Measure of Si )
proof end;
end;

:: deftheorem Def8 defines sigmaMeasureFamily MEASUR13:def 8 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for b4 being b1 -element FinSequence holds
( b4 is sigmaMeasureFamily of S iff for i being Nat st i in Seg m holds
ex Si being SigmaField of (X . i) st
( Si = S . i & b4 . i is sigma_Measure of Si ) );

definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
assume A1: n <= m ;
func SubFin (M,n) -> sigmaMeasureFamily of SubFin (S,n) equals :Def9: :: MEASUR13:def 9
M | n;
correctness
coherence
M | n is sigmaMeasureFamily of SubFin (S,n);
proof end;
end;

:: deftheorem Def9 defines SubFin MEASUR13:def 9 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
SubFin (M,n) = M | n;

definition
let m, n be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
assume A1: n <= m ;
func ElmFin (M,n) -> sigma_Measure of (ElmFin (S,n)) equals :Def10: :: MEASUR13:def 10
M . n;
correctness
coherence
M . n is sigma_Measure of (ElmFin (S,n));
proof end;
end;

:: deftheorem Def10 defines ElmFin MEASUR13:def 10 :
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
ElmFin (M,n) = M . n;

theorem Th3: :: MEASUR13:3
for m, i, j, k being non zero Nat
for X being non-empty b1 -element FinSequence st i <= j & j <= k & k <= m holds
(ProdFinSeq (SubFin (X,j))) . i = (ProdFinSeq (SubFin (X,k))) . i
proof end;

theorem Th4: :: MEASUR13:4
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n <= m holds
(ProdFinSeq X) . n = (ProdFinSeq (SubFin (X,n))) . n
proof end;

theorem Th5: :: MEASUR13:5
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n < m holds
(ProdFinSeq X) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):]
proof end;

theorem Th6: :: MEASUR13:6
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence holds CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):]
proof end;

theorem Th7: :: MEASUR13:7
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence st k <= n & n <= m holds
SubFin (X,k) = SubFin ((SubFin (X,n)),k)
proof end;

theorem Th8: :: MEASUR13:8
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence st k <= n & n <= m holds
ElmFin (X,k) = ElmFin ((SubFin (X,n)),k)
proof end;

theorem Th9: :: MEASUR13:9
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n < m holds
CarProduct (SubFin (X,(n + 1))) = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):]
proof end;

theorem :: MEASUR13:10
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence st n < m holds
(ProdFinSeq (SubFin (X,(n + 1)))) . (n + 1) = [:((ProdFinSeq (SubFin (X,n))) . n),(ElmFin (X,(n + 1))):]
proof end;

theorem :: MEASUR13:11
for n, i being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X st i <= n holds
CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i))
proof end;

theorem Th12: :: MEASUR13:12
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st k <= n & n <= m holds
ElmFin (S,k) = ElmFin ((SubFin (S,n)),k)
proof end;

theorem :: MEASUR13:13
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for Y being non-empty b2 -element FinSequence
for S being sigmaFieldFamily of X st n <= m & Y = X | n holds
SubFin (S,n) is sigmaFieldFamily of Y
proof end;

theorem Th14: :: MEASUR13:14
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st k <= n & n <= m holds
SubFin (S,k) = SubFin ((SubFin (S,n)),k)
proof end;

theorem :: MEASUR13:15
for m being non zero Nat
for X being non-empty b1 -element FinSequence ex F being Function of (CarProduct X),(product X) st
( F is one-to-one & F is onto )
proof end;

theorem :: MEASUR13:16
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for P being SemialgebraFamily of ProdFinSeq X st n <= m holds
P . n is semialgebra_of_sets of CarProduct (SubFin (X,n))
proof end;

theorem Th17: :: MEASUR13:17
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st k <= n & n <= m holds
ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)
proof end;

theorem Th18: :: MEASUR13:18
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st k <= n & n <= m holds
SubFin (M,k) = SubFin ((SubFin (M,n)),k)
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
func ProdSigmaFldFinSeq S -> sigmaFieldFamily of ProdFinSeq X means :Def11: :: MEASUR13:def 11
( it . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = it . i & it . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) );
existence
ex b1 being sigmaFieldFamily of ProdFinSeq X st
( b1 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = b1 . i & b1 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) )
proof end;
uniqueness
for b1, b2 being sigmaFieldFamily of ProdFinSeq X st b1 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = b1 . i & b1 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) & b2 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = b2 . i & b2 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines ProdSigmaFldFinSeq MEASUR13:def 11 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for b4 being sigmaFieldFamily of ProdFinSeq X holds
( b4 = ProdSigmaFldFinSeq S iff ( b4 . 1 = S . 1 & ( for i being non zero Nat st i < m holds
ex Si being SigmaField of (CarProduct (SubFin (X,i))) st
( Si = b4 . i & b4 . (i + 1) = sigma (measurable_rectangles (Si,(ElmFin (S,(i + 1))))) ) ) ) );

theorem Th19: :: MEASUR13:19
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
(ProdSigmaFldFinSeq S) . n is SigmaField of ((ProdFinSeq X) . n)
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
func Prod_Field S -> SigmaField of (CarProduct X) equals :: MEASUR13:def 12
(ProdSigmaFldFinSeq S) . m;
correctness
coherence
(ProdSigmaFldFinSeq S) . m is SigmaField of (CarProduct X);
by Th19;
end;

:: deftheorem defines Prod_Field MEASUR13:def 12 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X holds Prod_Field S = (ProdSigmaFldFinSeq S) . m;

theorem Th20: :: MEASUR13:20
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st k <= n & n <= m holds
(ProdSigmaFldFinSeq S) . k = (ProdSigmaFldFinSeq (SubFin (S,n))) . k
proof end;

theorem Th21: :: MEASUR13:21
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X st n < m holds
Prod_Field (SubFin (S,(n + 1))) = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
func ProdSigmaMesFinSeq M -> sigmaMeasureFamily of ProdSigmaFldFinSeq S means :Def13: :: MEASUR13:def 13
( it . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = it . i & it . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) );
existence
ex b1 being sigmaMeasureFamily of ProdSigmaFldFinSeq S st
( b1 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = b1 . i & b1 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) )
proof end;
uniqueness
for b1, b2 being sigmaMeasureFamily of ProdSigmaFldFinSeq S st b1 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = b1 . i & b1 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) & b2 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = b2 . i & b2 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 defines ProdSigmaMesFinSeq MEASUR13:def 13 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for b5 being sigmaMeasureFamily of ProdSigmaFldFinSeq S holds
( b5 = ProdSigmaMesFinSeq M iff ( b5 . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = b5 . i & b5 . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) ) );

theorem Th22: :: MEASUR13:22
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
(ProdSigmaMesFinSeq M) . n is sigma_Measure of (Prod_Field (SubFin (S,n)))
proof end;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
func Prod_Measure M -> sigma_Measure of (Prod_Field S) equals :: MEASUR13:def 14
(ProdSigmaMesFinSeq M) . m;
correctness
coherence
(ProdSigmaMesFinSeq M) . m is sigma_Measure of (Prod_Field S);
proof end;
end;

:: deftheorem defines Prod_Measure MEASUR13:def 14 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = (ProdSigmaMesFinSeq M) . m;

definition
let m be non zero Nat;
let X be non-empty m -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
attr M is sigma_finite means :: MEASUR13:def 15
 for i being Nat st i in Seg m holds
ex Xi being non empty set ex Si being SigmaField of Xi ex Mi being sigma_Measure of Si st
( Xi = X . i & Si = S . i & Mi = M . i & Mi is sigma_finite );
end;

:: deftheorem defines sigma_finite MEASUR13:def 15 :
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds
( M is sigma_finite iff for i being Nat st i in Seg m holds
ex Xi being non empty set ex Si being SigmaField of Xi ex Mi being sigma_Measure of Si st
( Xi = X . i & Si = S . i & Mi = M . i & Mi is sigma_finite ) );

theorem Th23: :: MEASUR13:23
for m, n, k being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st k <= n & n <= m holds
(ProdSigmaMesFinSeq (SubFin (M,n))) . k = (ProdSigmaMesFinSeq (SubFin (M,k))) . k
proof end;

theorem Th24: :: MEASUR13:24
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
(ProdSigmaMesFinSeq M) . n = Prod_Measure (SubFin (M,n))
proof end;

theorem Th25: :: MEASUR13:25
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
proof end;

theorem Th26: :: MEASUR13:26
for X being non empty set
for S being Field_Subset of X
for E being Set_Sequence of S
for i being Nat holds (Partial_Union E) . i in S
proof end;

theorem Th27: :: MEASUR13:27
for X, Y being non empty set
for S1 being SigmaField of X
for S2 being SigmaField of Y
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2 st M1 is sigma_finite & M2 is sigma_finite holds
Prod_Measure (M1,M2) is sigma_finite
proof end;

theorem Th28: :: MEASUR13:28
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
proof end;

theorem Th29: :: MEASUR13:29
for m being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st M is sigma_finite holds
Prod_Measure M is sigma_finite
proof end;

theorem Th30: :: MEASUR13:30
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m & M is sigma_finite holds
SubFin (M,n) is sigma_finite
proof end;

theorem Th31: :: MEASUR13:31
for m, n being non zero Nat
for X being non-empty b1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m & M is sigma_finite holds
ElmFin (M,n) is sigma_finite
proof end;

theorem Th32: :: MEASUR13:32
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st f is_integrable_on Prod_Measure M holds
ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) & Integral ((Prod_Measure M),f) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g) )
proof end;

theorem :: MEASUR13:33
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & f is_integrable_on Prod_Measure M & f = g & ( for y being Element of ElmFin (X,(n + 1)) holds (Integral1 ((Prod_Measure (SubFin (M,n))),|.g.|)) . y < +infty ) holds
( ( for y being Element of ElmFin (X,(n + 1)) holds ProjPMap2 (g,y) is_integrable_on Prod_Measure (SubFin (M,n)) ) & ( for V being Element of ElmFin (S,(n + 1)) holds Integral1 ((Prod_Measure (SubFin (M,n))),g) is V -measurable ) & Integral1 ((Prod_Measure (SubFin (M,n))),g) is_integrable_on ElmFin (M,(n + 1)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g) = Integral ((ElmFin (M,(n + 1))),(Integral1 ((Prod_Measure (SubFin (M,n))),g))) & Integral1 ((Prod_Measure (SubFin (M,n))),g) in L1_Functions (ElmFin (M,(n + 1))) )
proof end;

definition
let n be non zero Nat;
let X be non-empty n + 1 -element FinSequence;
let f be PartFunc of (CarProduct X),ExtREAL;
let x be Element of CarProduct (SubFin (X,n));
func ProjPMap1 (f,x) -> PartFunc of (ElmFin (X,(n + 1))),ExtREAL means :: MEASUR13:def 16
 ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & it = ProjPMap1 (g,x) );
existence
ex b1 being PartFunc of (ElmFin (X,(n + 1))),ExtREAL ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & b1 = ProjPMap1 (g,x) )
proof end;
uniqueness
for b1, b2 being PartFunc of (ElmFin (X,(n + 1))),ExtREAL st ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & b1 = ProjPMap1 (g,x) ) & ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & b2 = ProjPMap1 (g,x) ) holds
b1 = b2 ;
end;

:: deftheorem defines ProjPMap1 MEASUR13:def 16 :
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for f being PartFunc of (CarProduct X),ExtREAL
for x being Element of CarProduct (SubFin (X,n))
for b5 being PartFunc of (ElmFin (X,(n + 1))),ExtREAL holds
( b5 = ProjPMap1 (f,x) iff ex g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st
( f = g & b5 = ProjPMap1 (g,x) ) );

theorem Th34: :: MEASUR13:34
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1)))))
proof end;

theorem Th35: :: MEASUR13:35
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for fn1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & f = fn1 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.fn1.|)) . x < +infty ) holds
( Integral ((Prod_Measure M),f) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),fn1) & ( for x being Element of CarProduct (SubFin (X,n)) holds ProjPMap1 (fn1,x) is_integrable_on ElmFin (M,(n + 1)) ) & ( for U being Element of Prod_Field (SubFin (S,n)) holds Integral2 ((ElmFin (M,(n + 1))),fn1) is U -measurable ) & Integral2 ((ElmFin (M,(n + 1))),fn1) is_integrable_on Prod_Measure (SubFin (M,n)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),fn1) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),fn1))) & Integral2 ((ElmFin (M,(n + 1))),fn1) in L1_Functions (Prod_Measure (SubFin (M,n))) )
proof end;

theorem Th36: :: MEASUR13:36
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
proof end;

theorem :: MEASUR13:37
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
proof end;

definition
let n be non zero Nat;
let X be non-empty n + 1 -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
let f be PartFunc of (CarProduct X),ExtREAL;
func FSqIntg (M,f) -> n + 1 -element FinSequence means :Def17: :: MEASUR13:def 17
( it . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = it . i & it . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) );
existence
ex b1 being n + 1 -element FinSequence st
( b1 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = b1 . i & b1 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) )
proof end;
uniqueness
for b1, b2 being n + 1 -element FinSequence st b1 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = b1 . i & b1 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) & b2 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = b2 . i & b2 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def17 defines FSqIntg MEASUR13:def 17 :
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for b6 being b1 + 1 -element FinSequence holds
( b6 = FSqIntg (M,f) iff ( b6 . 1 = f & ( for i being Nat st 1 <= i & i < n + 1 holds
ex k being non zero Nat ex g being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL st
( k = (n + 1) - i & g = b6 . i & b6 . (i + 1) = Integral2 ((ElmFin (M,(k + 1))),g) ) ) ) );

definition
let n be non zero Nat;
let X be non-empty n + 1 -element FinSequence;
let S be sigmaFieldFamily of X;
let M be sigmaMeasureFamily of S;
let f be PartFunc of (CarProduct X),ExtREAL;
pred f is_Sequentially_integrable_on M means :: MEASUR13:def 18
 for k being non zero Nat st k < n + 1 holds
ex G being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL ex H being PartFunc of (CarProduct (SubFin (X,k))),ExtREAL st
( G = (FSqIntg (M,f)) . ((n + 1) - k) & H = (FSqIntg ((SubFin (M,(k + 1))),|.G.|)) . 2 & ( for x being Element of CarProduct (SubFin (X,k)) holds H . x < +infty ) );
end;

:: deftheorem defines is_Sequentially_integrable_on MEASUR13:def 18 :
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL holds
( f is_Sequentially_integrable_on M iff for k being non zero Nat st k < n + 1 holds
ex G being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL ex H being PartFunc of (CarProduct (SubFin (X,k))),ExtREAL st
( G = (FSqIntg (M,f)) . ((n + 1) - k) & H = (FSqIntg ((SubFin (M,(k + 1))),|.G.|)) . 2 & ( for x being Element of CarProduct (SubFin (X,k)) holds H . x < +infty ) ) );

theorem Th38: :: MEASUR13:38
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n + 1 holds
ex g being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL st
( g = (FSqIntg (M,f)) . ((n + 1) - k) & g is_integrable_on Prod_Measure (SubFin (M,(k + 1))) )
proof end;

theorem Th39: :: MEASUR13:39
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st f = g holds
( (FSqIntg (M,f)) . 1 = f & (FSqIntg (M,f)) . 2 = Integral2 ((ElmFin (M,(n + 1))),g) )
proof end;

theorem :: MEASUR13:40
for n being non zero Nat
for X being non-empty b1 + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL st M is sigma_finite & f is_Sequentially_integrable_on M & f is_integrable_on Prod_Measure M holds
for k being non zero Nat st k < n holds
ex Fk1 being PartFunc of [:(CarProduct (SubFin (X,k))),(ElmFin (X,(k + 1))):],ExtREAL ex Gk1 being PartFunc of (CarProduct (SubFin (X,(k + 1)))),ExtREAL ex Fk being Function of (CarProduct (SubFin (X,k))),ExtREAL st
( Gk1 = Fk1 & Gk1 = (FSqIntg (M,f)) . ((n + 1) - k) & Fk = (FSqIntg (M,f)) . ((n + 1) - (k - 1)) & Fk = Integral2 ((ElmFin (M,(k + 1))),Fk1) & Gk1 is_integrable_on Prod_Measure (SubFin (M,(k + 1))) & Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) & ( for x being Element of CarProduct (SubFin (X,k)) holds ProjPMap1 (Fk1,x) is_integrable_on ElmFin (M,(k + 1)) ) & ( for U being Element of Prod_Field (SubFin (S,k)) holds Fk is U -measurable ) & Fk is_integrable_on Prod_Measure (SubFin (M,k)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,k))),(ElmFin (M,(k + 1))))),Fk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) & Fk in L1_Functions (Prod_Measure (SubFin (M,k))) & Integral ((Prod_Measure (SubFin (M,(k + 1)))),Gk1) = Integral ((Prod_Measure (SubFin (M,k))),Fk) )
proof end;