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