let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x, y being Element of REAL st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is uniformly_continuous
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for x, y being Element of REAL st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is uniformly_continuous
let x, y be Element of REAL ; :: thesis: ( f is_uniformly_continuous_on dom f & f = g implies ProjPMap1 (g,[x,y]) is uniformly_continuous )
assume that
A1: f is_uniformly_continuous_on dom f and
A2: f = g ; :: thesis: ProjPMap1 (g,[x,y]) is uniformly_continuous
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for z1, z2 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for z1, z2 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for z1, z2 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for p1, p2 being Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] st p1 in dom f & p2 in dom f & ||.(p1 - p2).|| < s holds
||.((f /. p1) - (f /. p2)).|| < r by A1;

now :: thesis: for z1, z2 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r

let z1, z2 be Real; :: thesis: ( z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s implies |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r )
assume that
A5: z1 in dom (ProjPMap1 (g,[x,y])) and
A6: z2 in dom (ProjPMap1 (g,[x,y])) and
A7: |.(z1 - z2).| < s ; :: thesis: |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r
A8: X-section ((dom g),[x,y]) = { z where z is Element of REAL : [[x,y],z] in dom g } by MEASUR11:def 4;
A9: ( z1 in X-section ((dom g),[x,y]) & z2 in X-section ((dom g),[x,y]) ) by A5, A6, MESFUN12:def 3;
then A10: ex z being Element of REAL st
( z = z1 & [[x,y],z] in dom g ) by A8;
A11: ex z being Element of REAL st
( z = z2 & [[x,y],z] in dom g ) by A8, A9;
reconsider xx = x, yy = y as Point of RNS_Real ;
reconsider zz1 = z1 as Point of RNS_Real by XREAL_0:def 1;
reconsider zz2 = z2 as Point of RNS_Real by XREAL_0:def 1;
reconsider p1 = [xx,yy,zz1], p2 = [xx,yy,zz2] as Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] ;
A12: zz1 - zz2 = z1 - z2 by DUALSP03:4;
p1 - p2 = [xx,yy,zz1] + [(- xx),(- yy),(- zz2)] by PRVECT_4:9;
then p1 - p2 = [(xx - xx),(yy - yy),(zz1 - zz2)] by PRVECT_4:9;
then p1 - p2 = [(0. RNS_Real),(yy - yy),(zz1 - zz2)] by RLVECT_1:15;
then p1 - p2 = [(0. RNS_Real),(0. RNS_Real),(zz1 - zz2)] by RLVECT_1:15;
then ||.(p1 - p2).|| = sqrt (((||.(0. RNS_Real).|| ^2) + (||.(0. RNS_Real).|| ^2)) + (||.(zz1 - zz2).|| ^2)) by PRVECT_4:9;
then ||.(p1 - p2).|| = ||.(zz1 - zz2).|| by SQUARE_1:22;
then ||.(p1 - p2).|| = |.(z1 - z2).| by A12, EUCLID:def 2;
then A13: ||.((f /. p1) - (f /. p2)).|| < r by A4, A7, A2, A10, A11;
( (ProjPMap1 (g,[x,y])) . z1 = g . ([x,y],z1) & (ProjPMap1 (g,[x,y])) . z2 = g . ([x,y],z2) ) by A10, A11, MESFUN12:def 3;
then ( (ProjPMap1 (g,[x,y])) . z1 = f /. p1 & (ProjPMap1 (g,[x,y])) . z2 = f /. p2 ) by A2, A10, A11, PARTFUN1:def 6;
then ((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2) = (f /. p1) - (f /. p2) by DUALSP03:4;
hence |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r by A13, EUCLID:def 2; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1, z2 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & z2 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z2).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z2)).| < r ) ) by A3; :: thesis: verum

end;

hence ProjPMap1 (g,[x,y]) is uniformly_continuous by FCONT_2:def 1; :: thesis: verum