let n be non zero Nat; :: thesis: for E being set
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 E be set ; :: thesis: for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: for 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 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 yy1 = y1, yy2 = y2 as Point of RNS_Real by XREAL_0:def 1;
reconsider z1 = [x1,yy1], z2 = [x2,yy2] as Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] ;
- z2 = [(- x2),(- yy2)] by PRVECT_3:18;
then A6: z1 - z2 = [(x1 - x2),(yy1 - yy2)] by PRVECT_3:18;
A7: yy1 - yy2 = y1 - y2 by DUALSP03:4;
A8: ||.(x1 - x2).|| = ||.(x2 - x1).|| by NORMSP_1:7;
||.(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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 [:(CarProduct ((Seg n) --> 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 [:(CarProduct ((Seg n) --> 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 [:(CarProduct ((Seg n) --> 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 being Point of (CarProduct ((Seg n) --> RNS_Real))
for 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 [:(CarProduct ((Seg n) --> 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 [:(CarProduct ((Seg n) --> 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 [:(CarProduct ((Seg n) --> 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 [:(CarProduct ((Seg n) --> 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 x1 being Point of (CarProduct ((Seg n) --> RNS_Real)), yy1 being Point of RNS_Real such that
A16: z1 = [x1,yy1] by PRVECT_3:18;
consider x2 being Point of (CarProduct ((Seg n) --> RNS_Real)), yy2 being Point of RNS_Real such that
A17: z2 = [x2,yy2] by PRVECT_3:18;
reconsider y1 = yy1, y2 = yy2 as Real ;
- z2 = [(- x2),(- yy2)] by A17, PRVECT_3:18;
then A18: z1 - z2 = [(x1 - x2),(yy1 - yy2)] by A16, PRVECT_3:18;
A19: yy1 - yy2 = y1 - y2 by DUALSP03:4;
A20: ||.(x1 - x2).|| = ||.(x2 - x1).|| by NORMSP_1:7;
||.(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