let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for E being set 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, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for E being set 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, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )
let E be set ; :: 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, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < 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, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) )

hereby :: thesis: ( ( for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < 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, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) )
thus for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2, y1, y2, z1, z2 being Real st [x1,y1,z1] in E & [x2,y2,z2] in E & |.(x2 - x1).| < r & |.(y2 - y1).| < r & |.(z2 - z1).| < r holds
|.((g . [x2,y2,z2]) - (g . [x1,y1,z1])).| < e ) ) :: thesis: verum

proof

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

end;

end;

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

proof

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

proof

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

end;

end;

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