let I, J be closed_interval Subset of REAL; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f is_continuous_on [:I,J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:REAL,REAL:],REAL st f is_continuous_on [:I,J:] & f = g holds
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: ( f is_continuous_on [:I,J:] & f = g implies for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )
assume that
A1: f is_continuous_on [:I,J:] and
A2: f = g ; :: thesis: for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
f is_uniformly_continuous_on [:I,J:] by A1, Th9, NFCONT_2:10;
hence for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in [:I,J:] & [x2,y2] in [:I,J:] & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) by A2, Th10; :: thesis: verum