let E be set ; :: thesis: for f being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for g being PartFunc of [:REAL,REAL:],REAL st f = g & E c= dom f holds
( f is_uniformly_continuous_on E iff 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 E & [x2,y2] in E & |.(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 = g & E c= dom f holds
( f is_uniformly_continuous_on E iff 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis: ( f = g & E c= dom f implies ( f is_uniformly_continuous_on E iff 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) ) )
assume that
A1: f = g and
A2: E c= dom f ; :: thesis: ( f is_uniformly_continuous_on E iff 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )

hereby :: 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) ) implies f is_uniformly_continuous_on E )

assume A3: f is_uniformly_continuous_on E ; :: 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
thus 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) :: thesis: verum

proof

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
then consider r being Real such that
A4: ( 0 < r & ( for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e ) ) by A3;
set r1 = r / 2;
take r / 2 ; :: thesis: ( 0 < r / 2 & ( for x1, x2, y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r / 2 & |.(y2 - y1).| < r / 2 holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) )
thus 0 < r / 2 by A4, XREAL_1:215; :: thesis: for x1, x2, y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r / 2 & |.(y2 - y1).| < r / 2 holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e
let x1, x2, y1, y2 be Real; :: thesis: ( [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r / 2 & |.(y2 - y1).| < r / 2 implies |.((g . [x2,y2]) - (g . [x1,y1])).| < e )
assume A5: ( [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r / 2 & |.(y2 - y1).| < r / 2 ) ; :: thesis: |.((g . [x2,y2]) - (g . [x1,y1])).| < e
reconsider xx1 = x1, yy1 = y1, xx2 = x2, yy2 = y2 as Point of RNS_Real by XREAL_0:def 1;
reconsider z1 = [xx1,yy1], z2 = [xx2,yy2] as Point of [:RNS_Real,RNS_Real:] ;
- z2 = [(- xx2),(- yy2)] by PRVECT_3:18;
then A6: z1 - z2 = [(xx1 - xx2),(yy1 - yy2)] by PRVECT_3:18;
A7: ( xx1 - xx2 = x1 - x2 & yy1 - yy2 = y1 - y2 ) by DUALSP03:4;
then ||.(xx1 - xx2).|| = |.(x1 - x2).| by EUCLID:def 2;
then A8: ||.(xx1 - xx2).|| = |.(x2 - x1).| by COMPLEX1:60;
||.(yy1 - yy2).|| = |.(y1 - y2).| by A7, EUCLID:def 2;
then ||.(yy1 - yy2).|| = |.(y2 - y1).| by COMPLEX1:60;
then A9: ||.(z1 - z2).|| <= |.(x2 - x1).| + |.(y2 - y1).| by A6, A8, NDIFF_9:6;
|.(x2 - x1).| + |.(y2 - y1).| < (r / 2) + (r / 2) by A5, XREAL_1:8;
then ||.(z1 - z2).|| < r by A9, XXREAL_0:2;
then A10: ||.((f /. z1) - (f /. z2)).|| < e by A5, A4;
A11: f /. z1 = g . [x1,y1] by A1, A2, A5, PARTFUN1:def 6;
f /. z2 = f . z2 by A2, A5, PARTFUN1:def 6;
then (f /. z1) - (f /. z2) = (g . [x1,y1]) - (g . [x2,y2]) by A1, A11, DUALSP03:4;
then ||.((f /. z1) - (f /. z2)).|| = |.((g . [x1,y1]) - (g . [x2,y2])).| by EUCLID:def 2;
hence |.((g . [x2,y2]) - (g . [x1,y1])).| < e by A10, COMPLEX1:60; :: thesis: verum

end;

end;

assume A12: 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 E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) ; :: thesis: f is_uniformly_continuous_on E
for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e ) )

proof

let e be Real; :: thesis: ( 0 < e implies ex r being Real st
( 0 < r & ( for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e ) ) )
assume 0 < e ; :: thesis: ex r being Real st
( 0 < r & ( for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e ) )
then consider r being Real such that
A13: ( 0 < r & ( for x1, x2, y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) by A12;
take r ; :: thesis: ( 0 < r & ( for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e ) )
thus 0 < r by A13; :: thesis: for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e
thus for z1, z2 being Point of [:RNS_Real,RNS_Real:] st z1 in E & z2 in E & ||.(z1 - z2).|| < r holds
||.((f /. z1) - (f /. z2)).|| < e :: thesis: verum

proof

let z1, z2 be Point of [:RNS_Real,RNS_Real:]; :: thesis: ( z1 in E & z2 in E & ||.(z1 - z2).|| < r implies ||.((f /. z1) - (f /. z2)).|| < e )
assume that
A14: ( z1 in E & z2 in E ) and
A15: ||.(z1 - z2).|| < r ; :: thesis: ||.((f /. z1) - (f /. z2)).|| < e
consider xx1, yy1 being Point of RNS_Real such that
A16: z1 = [xx1,yy1] by PRVECT_3:18;
consider xx2, yy2 being Point of RNS_Real such that
A17: z2 = [xx2,yy2] by PRVECT_3:18;
reconsider x1 = xx1, y1 = yy1, x2 = xx2, y2 = yy2 as Real ;
- z2 = [(- xx2),(- yy2)] by A17, PRVECT_3:18;
then A18: z1 - z2 = [(xx1 - xx2),(yy1 - yy2)] by A16, PRVECT_3:18;
A19: ( xx1 - xx2 = x1 - x2 & yy1 - yy2 = y1 - y2 ) by DUALSP03:4;
then ||.(xx1 - xx2).|| = |.(x1 - x2).| by EUCLID:def 2;
then A20: ||.(xx1 - xx2).|| = |.(x2 - x1).| by COMPLEX1:60;
||.(yy1 - yy2).|| = |.(y1 - y2).| by A19, EUCLID:def 2;
then ||.(yy1 - yy2).|| = |.(y2 - y1).| by COMPLEX1:60;
then ( |.(x2 - x1).| <= ||.(z1 - z2).|| & |.(y2 - y1).| <= ||.(z1 - z2).|| ) by A18, A20, NDIFF_8:21;
then ( |.(x2 - x1).| < r & |.(y2 - y1).| < r ) by A15, XXREAL_0:2;
then A21: |.((g . [x2,y2]) - (g . [x1,y1])).| < e by A13, A14, A16, A17;
A22: f /. z1 = g . [x1,y1] by A1, A2, A14, A16, PARTFUN1:def 6;
f /. z2 = f . z2 by A2, A14, PARTFUN1:def 6;
then (f /. z1) - (f /. z2) = (g . [x1,y1]) - (g . [x2,y2]) by A1, A17, A22, DUALSP03:4;
then ||.((f /. z1) - (f /. z2)).|| = |.((g . [x1,y1]) - (g . [x2,y2])).| by EUCLID:def 2;
hence ||.((f /. z1) - (f /. z2)).|| < e by A21, COMPLEX1:60; :: thesis: verum

end;

end;

hence f is_uniformly_continuous_on E by A2; :: thesis: verum