:: Integrability of Multivariable Continuous Functions
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 12, 2025
:: Copyright (c) 2025-2026 Association of Mizar Users


theorem Th1: :: MESFUN18:1
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,REAL st dom f = {} holds
f is_integrable_on M
proof end;

theorem :: MESFUN18:2
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st dom f = {} holds
f is_integrable_on M
proof end;

:: WP: generalization \cite{MEASUR13}:3
theorem Th3: :: MESFUN18:3
for n, i, j, k being non zero Nat
for X being b1 -element FinSequence
for X1 being b3 -element FinSequence
for X2 being b4 -element FinSequence st i <= j & j <= k & X1 = X | j & X2 = X | k holds
(ProdFinSeq X1) . i = (ProdFinSeq X2) . i
proof end;

:: WP: generalization \cite{MEASUR13}:6
theorem Th4: :: MESFUN18:4
for n being non zero Nat
for D being b1 + 1 -element FinSequence
for D1 being b1 -element FinSequence st D1 = D | n holds
CarProduct D = [:(CarProduct D1),(D . (n + 1)):]
proof end;

Lm1: for I, J being Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st J is empty & [:I,J:] = dom f & f = g holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )
proof end;

:: WP: generalization \cite{MESFUN16}:51
theorem :: MESFUN18:5
for I being Subset of REAL
for J being closed_interval Subset of REAL
for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) | I is PartFunc of REAL,REAL & (Integral2 (L-Meas,(R_EAL g))) | I is PartFunc of REAL,REAL )
proof end;

:: WP: generalization \cite{MEASUR15}:51
theorem Th6: :: MESFUN18:6
for n being non zero Nat
for D being b1 -element FinSequence st not D is non-empty holds
CarProduct D = {}
proof end;

:: WP: generalization \cite{MEASUR15}:6
theorem Th7: :: MESFUN18:7
for n being non zero Nat
for X being b1 -element FinSequence
for x being object holds
( x in CarProduct X iff ex px being b1 -element FinSequence st
( px in product X & x = PtCarProduct px ) )
proof end;

:: WP: generalization \cite{MEASUR15}:39
theorem Th8: :: MESFUN18:8
for n being non zero Nat
for D being b1 -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Element of L-Field ) holds
CarProduct D is Element of Prod_Field (L-Field n)
proof end;

:: WP: generalization \cite{MEASUR15}:41
theorem Th9: :: MESFUN18:9
for n being non zero Nat
for D being b1 -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is Interval ) holds
CarProduct D is Element of Prod_Field (L-Field n)
proof end;

:: WP: generalization \cite{MEASUR15}:48
theorem Th10: :: MESFUN18:10
for n being non zero Nat
for X, Y being b1 -element FinSequence st ( for i being Nat st i in Seg n holds
X . i c= Y . i ) holds
CarProduct X c= CarProduct Y
proof end;

:: WP: generalization \cite{MEASUR15}:50
theorem Th11: :: MESFUN18:11
for n, k being non zero Nat
for X being non empty set
for D being b1 -element FinSequence st k in Seg n & ( for i being Nat st i in Seg n holds
D . i is Subset of X ) holds
(ProdFinSeq D) . k is Subset of (CarProduct ((Seg k) --> X))
proof end;

:: WP: generalization \cite{MEASUR15}:73
theorem Th12: :: MESFUN18:12
for n being non zero Nat
for D being b1 -element FinSequence st ( for i being Nat st i in Seg n holds
D . i c= REAL ) holds
product D = (CarProd ((Seg n) --> REAL)) .: (CarProduct D)
proof end;

theorem Th13: :: MESFUN18:13
( CarProduct ((Seg 1) --> RNS_Real) = RNS_Real & ElmFin (((Seg 1) --> RNS_Real),1) = RNS_Real & CarProduct ((Seg 2) --> RNS_Real) = [:RNS_Real,RNS_Real:] & ElmFin (((Seg 2) --> RNS_Real),2) = RNS_Real & CarProduct ((Seg 3) --> RNS_Real) = [:RNS_Real,RNS_Real,RNS_Real:] )
proof end;

theorem Th14: :: MESFUN18:14
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for p being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g holds
ProjPMap1 (g,p) is continuous
proof end;

theorem :: MESFUN18:15
for X, Y, Z being non empty set
for T being Function of X,Y
for f being PartFunc of X,Z
for g being PartFunc of Y,Z st T is bijective & g = f * (T ") holds
( dom g = T .: (dom f) & dom g = (.: T) . (dom f) )
proof end;

theorem Th16: :: MESFUN18:16
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (g,q) holds
P2 is_continuous_on dom P2
proof end;

theorem :: MESFUN18:17
for n being non zero Nat
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for q being Element of REAL holds
( (ProjPMap2 (g,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL & dom ((ProjPMap2 (g,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (g,q))) )
proof end;

theorem Th18: :: MESFUN18:18
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for p being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g holds
ProjPMap1 (|.g.|,p) is continuous
proof end;

theorem Th19: :: MESFUN18:19
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for q being Element of REAL st f is_continuous_on dom f & f = g & P2 = ProjPMap2 (|.g.|,q) holds
P2 is_continuous_on dom P2
proof end;

theorem :: MESFUN18:20
for n being non zero Nat
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for q being Element of REAL holds
( (ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ") is PartFunc of (REAL n),REAL & dom ((ProjPMap2 (|.g.|,q)) * ((CarProd ((Seg n) --> REAL)) ")) = (CarProd ((Seg n) --> REAL)) .: (dom (ProjPMap2 (|.g.|,q))) )
proof end;

theorem :: MESFUN18:21
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for p being Element of CarProduct ((Seg n) --> REAL) st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,p) is uniformly_continuous
proof end;

theorem :: MESFUN18:22
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for s being Element of REAL st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,s) holds
P2 is_uniformly_continuous_on dom P2
proof end;

theorem Th23: :: MESFUN18:23
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL
for x being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1 ((R_EAL g),x) holds
Pg1 is continuous
proof end;

theorem Th24: :: MESFUN18:24
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 ((R_EAL g),y) holds
Pg2 is_continuous_on dom Pg2
proof end;

theorem Th25: :: MESFUN18:25
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL
for x being Element of CarProduct ((Seg n) --> REAL) st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,x) holds
Pg1 is continuous
proof end;

theorem Th26: :: MESFUN18:26
for n being non zero Nat
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for y being Element of REAL st f is_continuous_on dom f & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
Pg2 is_continuous_on dom Pg2
proof end;

theorem Th27: :: MESFUN18:27
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 ((R_EAL g),x) holds
( Pg1 | J is bounded & Pg1 is_integrable_on J )
proof end;

theorem Th28: :: MESFUN18:28
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,x) holds
( Pg1 | J is bounded & Pg1 is_integrable_on J )
proof end;

theorem Th29: :: MESFUN18:29
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 ((R_EAL g),x) holds
Pg1 is_integrable_on L-Meas
proof end;

theorem Th30: :: MESFUN18:30
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 ((R_EAL g),x) holds
( integral (Pg1,J) = Integral (L-Meas,Pg1) & integral (Pg1,J) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),x))) & integral (Pg1,J) = (Integral2 (L-Meas,(R_EAL g))) . x )
proof end;

theorem Th31: :: MESFUN18:31
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,x) holds
Pg1 is_integrable_on L-Meas
proof end;

theorem Th32: :: MESFUN18:32
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & dom f = [:I,J:] & f is_continuous_on [:I,J:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,x) holds
( integral (Pg1,J) = Integral (L-Meas,Pg1) & integral (Pg1,J) = Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,x))) & integral (Pg1,J) = (Integral2 (L-Meas,|.(R_EAL g).|)) . x )
proof end;

theorem Th33: :: MESFUN18:33
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & E = [:I,J:] holds
g is E -measurable
proof end;

theorem Th34: :: MESFUN18:34
for n being non zero Nat
for I being Subset of (CarProduct ((Seg n) --> REAL))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL & Integral2 (L-Meas,(R_EAL g)) is PartFunc of (CarProduct ((Seg n) --> REAL)),REAL )
proof end;

theorem Th35: :: MESFUN18:35
for n being non zero Nat
for D being b1 -element FinSequence
for J being closed_interval Subset of REAL
for E being Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & E = [:(CarProduct D),J:] holds
E is compact
proof end;

theorem Th36: :: MESFUN18:36
for n being non zero Nat
for E being set
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & E c= dom f holds
( f is_uniformly_continuous_on E iff for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )
proof end;

theorem Th37: :: MESFUN18:37
for n being non zero Nat
for D being b1 -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f = g & f is_continuous_on [:(CarProduct D),J:] holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
proof end;

theorem Th38: :: MESFUN18:38
for X being set
for S being RealNormSpace
for f being PartFunc of S,RNS_Real
for g being PartFunc of X,REAL st f = g holds
||.f.|| = |.g.|
proof end;

theorem Th39: :: MESFUN18:39
for n being non zero Nat
for D being b1 -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on [:(CarProduct D),J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in [:(CarProduct D),J:] & [x2,y2] in [:(CarProduct D),J:] & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((|.g.| . [x2,y2]) - (|.g.| . [x1,y1])).| < e ) )
proof end;

Lm2: for a1, b1 being Real
for a2, b2 being R_eal st a1 = a2 & b1 = b2 holds
a1 - b1 = a2 - b2
proof end;

theorem Th40: :: MESFUN18:40
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,|.(R_EAL g).|)) | I holds
G2 is_continuous_on I
proof end;

theorem :: MESFUN18:41
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | I holds
G2 is_continuous_on I
proof end;

theorem Th42: :: MESFUN18:42
for n being non zero Nat
for D being b1 -element FinSequence
for g being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for f being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st f = g & g is_continuous_on CarProduct D & CarProduct D c= dom g & ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x, y being b1 -element FinSequence of REAL st PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D & ( for i being Nat st i in dom D holds
ex xi, yi being Real st
( xi = x . i & yi = y . i & |.(xi - yi).| < r ) ) holds
|.((f . (PtCarProduct x)) - (f . (PtCarProduct y))).| < e ) )
proof end;

theorem Th43: :: MESFUN18:43
for n being non zero Nat
for D being b1 -element FinSequence
for f being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st f = g & ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
g is_integrable_on Prod_Measure (L-Meas n)
proof end;

theorem Th44: :: MESFUN18:44
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & y in J & dom f = [:(CarProduct D),J:] & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( dom (ProjPMap2 ((R_EAL g),y)) = CarProduct D & ProjPMap2 ((R_EAL g),y) is_integrable_on Prod_Measure (L-Meas n) )
proof end;

theorem Th45: :: MESFUN18:45
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & y in J & dom f = [:(CarProduct D),J:] & f is_continuous_on [:(CarProduct D),J:] & f = g & Pg2 = ProjPMap2 ((R_EAL g),y) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 ((R_EAL g),y))) = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) . y )
proof end;

theorem Th46: :: MESFUN18:46
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & y in J & dom f = [:(CarProduct D),J:] & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( dom (ProjPMap2 (|.(R_EAL g).|,y)) = CarProduct D & ProjPMap2 (|.(R_EAL g).|,y) is_integrable_on Prod_Measure (L-Meas n) )
proof end;

theorem Th47: :: MESFUN18:47
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for E being Element of Prod_Field (L-Field n) st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & y in J & dom f = [:(CarProduct D),J:] & f is_continuous_on [:(CarProduct D),J:] & f = g & E = CarProduct D holds
ProjPMap2 (|.(R_EAL g).|,y) is E -measurable
proof end;

theorem Th48: :: MESFUN18:48
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for y being Element of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Pg2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & y in J & dom f = [:(CarProduct D),J:] & f is_continuous_on [:(CarProduct D),J:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,y) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas n)),(ProjPMap2 (|.(R_EAL g).|,y))) = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y )
proof end;

theorem Th49: :: MESFUN18:49
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being Interval st ( for i being Nat st i in Seg n holds
D . i is Interval ) & I = CarProduct D holds
( [:I,J:] is Subset of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] & [:I,J:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) )
proof end;

theorem Th50: :: MESFUN18:50
for n being non zero Nat
for D being b1 -element FinSequence
for J being Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g holds
( (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J is PartFunc of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J is PartFunc of REAL,REAL )
proof end;

theorem Th51: :: MESFUN18:51
for n being non zero Nat
for E1 being Element of Prod_Field (L-Field n)
for E2 being Element of L-Field holds
( [:E1,E2:] in sigma (measurable_rectangles ((Prod_Field (L-Field n)),L-Field)) & (Prod_Measure (L-Meas (n + 1))) . [:E1,E2:] = ((Prod_Measure (L-Meas n)) . E1) * (L-Meas . E2) )
proof end;

theorem Th52: :: MESFUN18:52
for n being non zero Nat
for D being b1 -element FinSequence st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) holds
ex r being Real ex E being Element of Prod_Field (L-Field n) st
( E = CarProduct D & (Prod_Measure (L-Meas n)) . E = r & 0 <= r )
proof end;

theorem Th53: :: MESFUN18:53
for n being non zero Nat
for D being b1 -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) | J holds
G1 is continuous
proof end;

theorem Th54: :: MESFUN18:54
for n being non zero Nat
for D being b1 -element FinSequence
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & [:(CarProduct D),J:] = dom f & f is_continuous_on [:(CarProduct D),J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
G1 is continuous
proof end;

Lm3: for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) )
proof end;

Lm4: for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for y being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) )
proof end;

theorem :: MESFUN18:55
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for y being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is V -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas n) & Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) ) by Lm3, Lm4;

theorem Th56: :: MESFUN18:56
for n being non zero Nat
for D being b1 + 1 -element FinSequence
for f being PartFunc of (CarProduct ((Seg (n + 1)) --> RNS_Real)),RNS_Real
for g being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & g0 = g & ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
( Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),g) = Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g0) )
proof end;

theorem :: MESFUN18:57
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G2 being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G2 = (Integral2 (L-Meas,(R_EAL g))) | (CarProduct D) holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = Integral ((Prod_Measure (L-Meas n)),G2)
proof end;

theorem :: MESFUN18:58
for n being non zero Nat
for D being b1 -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being non empty closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for G1 being PartFunc of REAL,REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g & G1 = (Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g))) | J holds
Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),(R_EAL g)) = integral (G1,J)
proof end;

theorem :: MESFUN18:59
for n being non zero Nat
for f being PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real holds f * (CarProd ((Seg n) --> RNS_Real)) is PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real ;

theorem Th60: :: MESFUN18:60
for n being non zero Nat
for D being b1 -element FinSequence
for f being PartFunc of (product ((Seg n) --> RNS_Real)),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is Subset of REAL ) & f is_continuous_on dom f & dom f = product D holds
f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D
proof end;

theorem Th61: :: MESFUN18:61
for n being non zero Nat holds
( REAL-NS n = product ((Seg n) --> RNS_Real) & REAL n = the carrier of (product ((Seg n) --> RNS_Real)) & REAL n = product ((Seg n) --> REAL) )
proof end;

theorem Th62: :: MESFUN18:62
for n being non zero Nat
for D being b1 -element FinSequence
for f being PartFunc of (REAL-NS n),RNS_Real st ( for i being Nat st i in Seg n holds
D . i is Subset of REAL ) & f is_continuous_on dom f & dom f = product D holds
f * (CarProd ((Seg n) --> RNS_Real)) is_continuous_on CarProduct D
proof end;

theorem :: MESFUN18:63
for n being non zero Nat
for D being b1 -element FinSequence
for f being PartFunc of (REAL-NS n),RNS_Real
for g being PartFunc of (REAL n),REAL
for G being PartFunc of (CarProduct ((Seg n) --> REAL)),REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & g = f & G = f * (CarProd ((Seg n) --> REAL)) holds
( G is_integrable_on Prod_Measure (L-Meas n) & g is_integrable_on XL-Meas n & Integral ((XL-Meas n),g) = Integral ((Prod_Measure (L-Meas n)),G) )
proof end;

theorem :: MESFUN18:64
for n being non zero Nat
for D being b1 + 1 -element FinSequence
for f being PartFunc of (REAL-NS (n + 1)),RNS_Real
for G being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & G = f * (CarProd ((Seg (n + 1)) --> REAL)) & g0 = G holds
( ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g0).|)) . x < +infty ) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds ProjPMap1 ((R_EAL g0),x) is_integrable_on L-Meas ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g0)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),G) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g0)))) )
proof end;

theorem :: MESFUN18:65
for n being non zero Nat
for D being b1 + 1 -element FinSequence
for D1 being b1 -element FinSequence
for f being PartFunc of (REAL-NS (n + 1)),RNS_Real
for G being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL
for Dk1 being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for Pg being PartFunc of REAL,REAL st D1 = D | n & ( for i being Nat st i in Seg (n + 1) holds
D . i is Subset of REAL ) & f is_continuous_on product D & dom f = product D & G = f * (CarProd ((Seg (n + 1)) --> REAL)) & g0 = G & Dk1 = D . (n + 1) & x in CarProduct D1 & Pg = ProjPMap1 (|.(R_EAL g0).|,x) holds
( dom (ProjPMap1 (|.(R_EAL g0).|,x)) = D . (n + 1) & Pg | Dk1 is continuous & Pg | Dk1 is bounded & Pg is_integrable_on Dk1 & ProjPMap1 (|.(R_EAL g0).|,x) is_integrable_on L-Meas & Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) = integral (Pg,Dk1) & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = integral (Pg,Dk1) )
proof end;