theorem
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:])))) )