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 ) )