theorem Th36:
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