:: Integral of Continuous Three Variable Functions
:: by Noboru Endou and Yasunari Shidama
::
:: Received June 18, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

Lm1: for x, a being Real ex r being Real st
( 0 < r & x in ].(a - r),(a + r).[ )

proof end;

Lm2: for x, a, b being Real st a <= b holds
].(x - a),(x + a).[ c= ].(x - b),(x + b).[

proof end;

theorem Th1: :: MESFUN17:1

for X, Y, Z being RealNormSpace
for u being Point of [:X,Y,Z:]
for x being Point of X
for y being Point of Y
for z being Point of Z st u = [x,y,z] holds
( ||.u.|| <= (||.x.|| + ||.y.||) + ||.z.|| & ||.x.|| <= ||.u.|| & ||.y.|| <= ||.u.|| & ||.z.|| <= ||.u.|| )

proof end;

theorem Th2: :: MESFUN17:2

for I, J, K being closed_interval Subset of REAL
for E being Subset of [:[:RNS_Real,RNS_Real:],RNS_Real:] st E = [:[:I,J:],K:] holds
E is compact

proof end;

theorem Th3: :: MESFUN17:3

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being set 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, y1, y2, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )

proof end;

theorem Th4: :: MESFUN17:4

for I, J, K being Interval holds
( [:[:I,J:],K:] is Subset of [:[:RNS_Real,RNS_Real:],RNS_Real:] & [:[:I,J:],K:] in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) )

proof end;

theorem Th5: :: MESFUN17:5

for u being Point of [:RNS_Real,RNS_Real,RNS_Real:]
for r being Real st 0 < r holds
ex s, x, y, z being Real st
( 0 < s & s < r & u = [x,y,z] & [:].(x - s),(x + s).[,].(y - s),(y + s).[,].(z - s),(z + s).[:] c= Ball (u,r) )

proof end;

theorem Th6: :: MESFUN17:6

for A being Subset of [:RNS_Real,RNS_Real,RNS_Real:] st ( for a, b, c being Real st [a,b,c] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } ) ) holds
ex F being Function of A,REAL st
for a, b, c being Real st [a,b,c] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[,].(c - r),(c + r).[:] c= A ) } & F . [a,b,c] = (upper_bound Rx) / 2 )

proof end;

Lm3: for A being set st A c= [:REAL,REAL,REAL:] & A /\ [:RAT,RAT,RAT:] <> {} holds
ex p being sequence of [:REAL,REAL,REAL:] st rng p = A /\ [:RAT,RAT,RAT:]

proof end;

theorem Th7: :: MESFUN17:7

for A being Subset of [:RNS_Real,RNS_Real,RNS_Real:] st A is open holds
A in sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field))

proof end;

theorem Th8: :: MESFUN17:8

for I, J, K being closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )

proof end;

theorem Th9: :: MESFUN17:9

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f = g holds
||.f.|| = |.g.|

proof end;

theorem Th10: :: MESFUN17:10

for I, J, K being closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st x1 in I & x2 in I & y1 in J & y2 in J & z1 in K & z2 in K & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((|.g.| . [x2,y2,z2]) - (|.g.| . [x1,y1,z1])).| < e ) )

proof end;

theorem Th11: :: MESFUN17:11

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x, y being Element of REAL st f is_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is continuous

proof end;

theorem Th12: :: MESFUN17:12

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_continuous_on dom p2

proof end;

theorem Th13: :: MESFUN17:13

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x, y being Element of REAL st f is_continuous_on dom f & f = g holds
ProjPMap1 (|.g.|,[x,y]) is continuous

proof end;

theorem Th14: :: MESFUN17:14

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_continuous_on dom f & f = g & p2 = ProjPMap2 (|.g.|,z) holds
p2 is_continuous_on dom p2

proof end;

theorem :: MESFUN17:15

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x, y being Element of REAL st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is uniformly_continuous

proof end;

theorem :: MESFUN17:16

for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_uniformly_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_uniformly_continuous_on dom p2

proof end;

theorem Th17: :: MESFUN17:17

for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1 ((R_EAL g),[x,y]) holds
Pg1 is continuous

proof end;

theorem Th18: :: MESFUN17:18

for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 ((R_EAL g),z) holds
Pf2 is_continuous_on dom Pf2

proof end;

theorem Th19: :: MESFUN17:19

for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st f is_continuous_on dom f & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,[x,y]) holds
Pg1 is continuous

proof end;

theorem Th20: :: MESFUN17:20

for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pf2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st f is_continuous_on dom f & f = g & Pf2 = ProjPMap2 (|.(R_EAL g).|,z) holds
Pf2 is_continuous_on dom Pf2

proof end;

theorem Th21: :: MESFUN17:21

for I, J being Subset of REAL
for K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & y in J & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg1 = ProjPMap1 ((R_EAL g),[x,y]) holds
( Pg1 | K is bounded & Pg1 is_integrable_on K )

proof end;

theorem Th22: :: MESFUN17:22

for I, J being Subset of REAL
for K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & y in J & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg1 = ProjPMap1 ((R_EAL g),[x,y]) holds
( Pg1 is_integrable_on L-Meas & integral (Pg1,K) = Integral (L-Meas,Pg1) & integral (Pg1,K) = Integral (L-Meas,(ProjPMap1 ((R_EAL g),[x,y]))) & integral (Pg1,K) = (Integral2 (L-Meas,(R_EAL g))) . [x,y] )

proof end;

theorem Th23: :: MESFUN17:23

for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 ((R_EAL g),z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 ((R_EAL g),z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z )

proof end;

theorem Th24: :: MESFUN17:24

for I, J being Subset of REAL
for K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & y in J & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,[x,y]) holds
( Pg1 | K is bounded & Pg1 is_integrable_on K )

proof end;

theorem Th25: :: MESFUN17:25

for I, J being Subset of REAL
for K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL
for E being Element of L-Field st x in I & y in J & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,[x,y]) & E = K holds
Pg1 is E -measurable

proof end;

theorem Th26: :: MESFUN17:26

for I, J being Subset of REAL
for K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg1 being PartFunc of REAL,REAL st x in I & y in J & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg1 = ProjPMap1 (|.(R_EAL g).|,[x,y]) holds
( Pg1 is_integrable_on L-Meas & integral (Pg1,K) = Integral (L-Meas,Pg1) & integral (Pg1,K) = Integral (L-Meas,(ProjPMap1 (|.(R_EAL g).|,[x,y]))) & integral (Pg1,K) = (Integral2 (L-Meas,|.(R_EAL g).|)) . [x,y] )

proof end;

theorem Th27: :: MESFUN17:27

for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL
for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) & E = [:I,J:] holds
Pg2 is E -measurable

proof end;

theorem Th28: :: MESFUN17:28

for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )

proof end;

theorem Th29: :: MESFUN17:29

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of sigma (measurable_rectangles ((sigma (measurable_rectangles (L-Field,L-Field))),L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & E = [:[:I,J:],K:] holds
g is E -measurable

proof end;

theorem Th30: :: MESFUN17:30

for I, J, K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 (|.(R_EAL g).|,u2)) . z) - ((ProjPMap1 (|.(R_EAL g).|,u1)) . z)).| < e ) )

proof end;

theorem Th31: :: MESFUN17:31

for I, J, K being non empty closed_interval Subset of REAL
for x, y being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for u1, u2 being Element of [:REAL,REAL:]
for x1, y1, x2, y2 being Real st u1 = [x1,y1] & u2 = [x2,y2] & |.(x2 - x1).| < r & |.(y2 - y1).| < r & u1 in [:I,J:] & u2 in [:I,J:] holds
for z being Element of REAL st z in K holds
|.(((ProjPMap1 ((R_EAL g),u2)) . z) - ((ProjPMap1 ((R_EAL g),u1)) . z)).| < e ) )

proof end;

Lm4: for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for v being Element of [:REAL,REAL:]
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f = g & not v in [:I,J:] holds
( (Integral2 (L-Meas,|.(R_EAL g).|)) . v = 0 & (Integral2 (L-Meas,(R_EAL g))) . v = 0 )

proof end;

Lm5: for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f = g & not z in K holds
( (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z = 0 & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) . z = 0 )

proof end;

theorem Th32: :: MESFUN17:32

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral2 (L-Meas,|.(R_EAL g).|) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL & Integral2 (L-Meas,(R_EAL g)) is Function of [:REAL,REAL:],REAL & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is PartFunc of [:REAL,REAL:],REAL )

proof end;

theorem Th33: :: MESFUN17:33

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Fz being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,|.(R_EAL g).|)) | [:I,J:] holds
Fz is_uniformly_continuous_on [:I,J:]

proof end;

theorem Th34: :: MESFUN17:34

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Fz being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Fz = (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] holds
Fz is_uniformly_continuous_on [:I,J:]

proof end;

theorem Th35: :: MESFUN17:35

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K is PartFunc of REAL,REAL & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is Function of REAL,REAL & (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K is PartFunc of REAL,REAL )

proof end;

Lm6: for a, b being Real
for x, y being ExtReal st a = x & b = y holds
a - b = x - y

proof end;

theorem Th36: :: MESFUN17:36

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) | K holds
Gxy is continuous

proof end;

theorem Th37: :: MESFUN17:37

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K holds
Gxy is continuous

proof end;

theorem Th38: :: MESFUN17:38

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is nonnegative

proof end;

theorem Th39: :: MESFUN17:39

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is nonnegative

proof end;

theorem Th40: :: MESFUN17:40

for I, J, K being non empty closed_interval Subset of REAL
for u being Element of [:REAL,REAL:]
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
(Integral2 (L-Meas,|.(R_EAL g).|)) . u < +infty

proof end;

theorem Th41: :: MESFUN17:41

for I, J, K being non empty closed_interval Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
(Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z < +infty

proof end;

theorem Th42: :: MESFUN17:42

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable

proof end;

theorem Th43: :: MESFUN17:43

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas) & ( for u being Element of [:REAL,REAL:] holds ProjPMap1 ((R_EAL g),u) is_integrable_on L-Meas ) & ( for U being Element of sigma (measurable_rectangles (L-Field,L-Field)) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) )

proof end;

theorem :: MESFUN17:44

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for z being Element of REAL holds ProjPMap2 ((R_EAL g),z) is_integrable_on Prod_Measure (L-Meas,L-Meas) ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is V -measurable ) & Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g)))) )

proof end;

theorem Th45: :: MESFUN17:45

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & x in I holds
ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is E -measurable

proof end;

theorem Th46: :: MESFUN17:46

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for x being Element of REAL holds (Integral2 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . x < +infty ) & ( for x being Element of REAL holds ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is_integrable_on L-Meas ) )

proof end;

theorem Th47: :: MESFUN17:47

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for y being Element of REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & y in J holds
ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is E -measurable

proof end;

theorem Th48: :: MESFUN17:48

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for y being Element of REAL holds (Integral1 (L-Meas,|.(Integral2 (L-Meas,(R_EAL g))).|)) . y < +infty ) & ( for y being Element of REAL holds ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is_integrable_on L-Meas ) )

proof end;

theorem :: MESFUN17:49

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of sigma (measurable_rectangles (L-Field,L-Field)) st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral2 (L-Meas,|.(R_EAL g).|) is E -measurable

proof end;

theorem :: MESFUN17:50

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being Element of L-Field st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|) is E -measurable

proof end;

theorem :: MESFUN17:51

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x) is Function of REAL,REAL & ProjPMap1 (|.(Integral2 (L-Meas,(R_EAL g))).|,x) is Function of REAL,REAL )

proof end;

theorem :: MESFUN17:52

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for y being Element of REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y) is Function of REAL,REAL & ProjPMap2 (|.(Integral2 (L-Meas,(R_EAL g))).|,y) is Function of REAL,REAL )

proof end;

theorem :: MESFUN17:53

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
|.(Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))).| is Function of REAL,REAL

proof end;

theorem Th54: :: MESFUN17:54

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | (REAL \ J))) = 0

proof end;

theorem Th55: :: MESFUN17:55

for y being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | (REAL \ I))) = 0

proof end;

theorem :: MESFUN17:56

for I, J, K being non empty closed_interval Subset of REAL
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom g holds
Integral (L-Meas,((Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | (REAL \ K))) = 0

proof end;

theorem :: MESFUN17:57

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
P1Gz is continuous

proof end;

theorem :: MESFUN17:58

for y being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
P2Gz is continuous

proof end;

theorem Th59: :: MESFUN17:59

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( P1Gz || J is bounded & P1Gz is_integrable_on J )

proof end;

theorem Th60: :: MESFUN17:60

for y being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( P2Gz || I is bounded & P2Gz is_integrable_on I )

proof end;

theorem :: MESFUN17:61

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gxy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gxy = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),(R_EAL g))) | K holds
( Gxy || K is bounded & Gxy is_integrable_on K )

proof end;

theorem :: MESFUN17:62

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J holds
( (ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J is_integrable_on L-Meas & integral (P1Gz,J) = Integral (L-Meas,((ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x)) | J)) & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 ((Integral2 (L-Meas,(R_EAL g))),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . x )

proof end;

theorem :: MESFUN17:63

for y being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I holds
( (ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I is_integrable_on L-Meas & integral (P2Gz,I) = Integral (L-Meas,((ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y)) | I)) & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 ((Integral2 (L-Meas,(R_EAL g))),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g))))) . y )

proof end;

theorem :: MESFUN17:64

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for U being Element of L-Field holds Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is U -measurable ) & Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral2 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & (Integral2 (L-Meas,(R_EAL g))) | [:I,J:] is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )

proof end;

theorem :: MESFUN17:65

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g holds
( ( for V being Element of L-Field holds Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is V -measurable ) & Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))) is_integrable_on L-Meas & Integral ((Prod_Measure (L-Meas,L-Meas)),(Integral2 (L-Meas,(R_EAL g)))) = Integral (L-Meas,(Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas,L-Meas)),L-Meas)),g) = Integral (L-Meas,(Integral1 (L-Meas,(Integral2 (L-Meas,(R_EAL g)))))) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = Integral (L-Meas,(Integral1 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])))) )

proof end;

theorem :: MESFUN17:66

for x being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P1Gz being PartFunc of REAL,REAL st x in I & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P1Gz = ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x) holds
( P1Gz is continuous & dom (ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x)) = J & P1Gz | J is bounded & P1Gz is_integrable_on J & integral (P1Gz,J) = Integral (L-Meas,(ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x))) & integral (P1Gz,J) = (Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) . x & ProjPMap1 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),x) is_integrable_on L-Meas )

proof end;

theorem :: MESFUN17:67

for y being Element of REAL
for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for P2Gz being PartFunc of REAL,REAL st y in J & [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & P2Gz = ProjPMap2 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),y) holds
( P2Gz is continuous & dom (ProjPMap2 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),y)) = I & P2Gz | I is bounded & P2Gz is_integrable_on I & integral (P2Gz,I) = Integral (L-Meas,(ProjPMap2 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),y))) & integral (P2Gz,I) = (Integral1 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) . y & ProjPMap2 (((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]),y) is_integrable_on L-Meas )

proof end;

theorem :: MESFUN17:68

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gzy being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gzy = (Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | I holds
( dom Gzy = I & Gzy is continuous & Gzy || I is bounded & Gzy is_integrable_on I & (Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | I is_integrable_on L-Meas & Integral (L-Meas,((Integral2 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | I)) = integral (Gzy,I) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = integral (Gzy,I) )

proof end;

theorem :: MESFUN17:69

for I, J, K being non empty closed_interval Subset of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Gzx being PartFunc of REAL,REAL st [:[:I,J:],K:] = dom f & f is_continuous_on [:[:I,J:],K:] & f = g & Gzx = (Integral1 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | J holds
( dom Gzx = J & Gzx is continuous & Gzx || J is bounded & Gzx is_integrable_on J & (Integral1 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | J is_integrable_on L-Meas & Integral (L-Meas,((Integral1 (L-Meas,((Integral2 (L-Meas,(R_EAL g))) | [:I,J:]))) | J)) = integral (Gzx,J) & Integral ((Prod_Measure (L-Meas,L-Meas)),((Integral2 (L-Meas,(R_EAL g))) | [:I,J:])) = integral (Gzx,J) )

proof end;