let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_uniformly_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_uniformly_continuous_on dom p2
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for p2 being PartFunc of [:RNS_Real,RNS_Real:],RNS_Real
for z being Element of REAL st f is_uniformly_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_uniformly_continuous_on dom p2
let p2 be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis: for z being Element of REAL st f is_uniformly_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_uniformly_continuous_on dom p2
let z be Element of REAL ; :: thesis: ( f is_uniformly_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) implies p2 is_uniformly_continuous_on dom p2 )
assume that
A1: f is_uniformly_continuous_on dom f and
A2: f = g and
A3: p2 = ProjPMap2 (g,z) ; :: thesis: p2 is_uniformly_continuous_on dom p2
reconsider zz = z as Point of RNS_Real ;
A4: Y-section ((dom g),z) = { t where t is Element of [:RNS_Real,RNS_Real:] : [t,z] in dom g } by MEASUR11:def 5;

now :: thesis: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for xy1, xy2 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s holds
||.((p2 /. xy1) - (p2 /. xy2)).|| < r ) )

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for xy1, xy2 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s holds
||.((p2 /. xy1) - (p2 /. xy2)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for xy1, xy2 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s holds
||.((p2 /. xy1) - (p2 /. xy2)).|| < r ) )
then consider s being Real such that
A5: 0 < s and
A6: for v1, v2 being Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] st v1 in dom f & v2 in dom f & ||.(v1 - v2).|| < s holds
||.((f /. v1) - (f /. v2)).|| < r by A1;
take s = s; :: thesis: ( 0 < s & ( for xy1, xy2 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s holds
||.((p2 /. xy1) - (p2 /. xy2)).|| < r ) )
thus 0 < s by A5; :: thesis: for xy1, xy2 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s holds
||.((p2 /. xy1) - (p2 /. xy2)).|| < r

hereby :: thesis: verum

let xy1, xy2 be Point of [:RNS_Real,RNS_Real:]; :: thesis: ( xy1 in dom p2 & xy2 in dom p2 & ||.(xy1 - xy2).|| < s implies ||.((p2 /. xy1) - (p2 /. xy2)).|| < r )
assume that
A7: ( xy1 in dom p2 & xy2 in dom p2 ) and
A8: ||.(xy1 - xy2).|| < s ; :: thesis: ||.((p2 /. xy1) - (p2 /. xy2)).|| < r
A9: ( xy1 in Y-section ((dom g),z) & xy2 in Y-section ((dom g),z) ) by A3, A7, MESFUN12:def 4;
then A10: ex t1 being Element of [:RNS_Real,RNS_Real:] st
( t1 = xy1 & [t1,z] in dom g ) by A4;
A11: ex t2 being Element of [:RNS_Real,RNS_Real:] st
( t2 = xy2 & [t2,z] in dom g ) by A4, A9;
consider xx1, yy1 being Point of RNS_Real such that
A12: xy1 = [xx1,yy1] by PRVECT_3:18;
consider xx2, yy2 being Point of RNS_Real such that
A13: xy2 = [xx2,yy2] by PRVECT_3:18;
reconsider x1 = xx1, y1 = yy1, x2 = xx2, y2 = yy2 as Real ;
reconsider v1 = [xx1,yy1,zz], v2 = [xx2,yy2,zz] as Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] ;
v1 - v2 = [xx1,yy1,zz] + [(- xx2),(- yy2),(- zz)] by PRVECT_4:9;
then v1 - v2 = [(xx1 - xx2),(yy1 - yy2),(zz - zz)] by PRVECT_4:9;
then v1 - v2 = [(xx1 - xx2),(yy1 - yy2),(0. RNS_Real)] by RLVECT_1:15;
then A14: ||.(v1 - v2).|| = sqrt (((||.(xx1 - xx2).|| ^2) + (||.(yy1 - yy2).|| ^2)) + (||.(0. RNS_Real).|| ^2)) by PRVECT_4:9;
xy1 - xy2 = [xx1,yy1] + [(- xx2),(- yy2)] by A12, A13, PRVECT_3:18;
then xy1 - xy2 = [(xx1 - xx2),(yy1 - yy2)] by PRVECT_3:18;
then ||.(xy1 - xy2).|| = sqrt ((||.(xx1 - xx2).|| ^2) + (||.(yy1 - yy2).|| ^2)) by NDIFF_8:1;
then A15: ||.((f /. v1) - (f /. v2)).|| < r by A2, A6, A8, A10, A11, A12, A13, A14;
p2 /. xy1 = (ProjPMap2 (g,z)) . xy1 by A3, A7, PARTFUN1:def 6;
then p2 /. xy1 = g . ([x1,y1],z) by A10, A12, MESFUN12:def 4;
then A16: p2 /. xy1 = f /. v1 by A2, A10, A12, PARTFUN1:def 6;
p2 /. xy2 = (ProjPMap2 (g,z)) . xy2 by A3, A7, PARTFUN1:def 6;
then p2 /. xy2 = g . ([x2,y2],z) by A13, A11, MESFUN12:def 4;
hence ||.((p2 /. xy1) - (p2 /. xy2)).|| < r by A2, A11, A13, A15, A16, PARTFUN1:def 6; :: thesis: verum

end;

end;

hence p2 is_uniformly_continuous_on dom p2 ; :: thesis: verum