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

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for y1, y2 being Real st y1 in dom (ProjPMap1 (g,t)) & y2 in dom (ProjPMap1 (g,t)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,t)) . y1) - ((ProjPMap1 (g,t)) . y2)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y1, y2 being Real st y1 in dom (ProjPMap1 (g,t)) & y2 in dom (ProjPMap1 (g,t)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,t)) . y1) - ((ProjPMap1 (g,t)) . y2)).| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for p1, p2 being Point of [: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 y1, y2 being Real st y1 in dom (ProjPMap1 (g,t)) & y2 in dom (ProjPMap1 (g,t)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,t)) . y1) - ((ProjPMap1 (g,t)) . y2)).| < r

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

end;

hence ex s being Real st
( 0 < s & ( for y1, y2 being Real st y1 in dom (ProjPMap1 (g,t)) & y2 in dom (ProjPMap1 (g,t)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,t)) . y1) - ((ProjPMap1 (g,t)) . y2)).| < r ) ) by A3; :: thesis: verum

end;

hence ProjPMap1 (g,t) is uniformly_continuous by FCONT_2:def 1; :: thesis: ProjPMap2 (g,t) is uniformly_continuous
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r ) )
then consider s being Real such that
A14: 0 < s and
A15: for p1, p2 being Point of [: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 x1, x2 being Real st x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r

let x1, x2 be Real; :: thesis: ( x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s implies |.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r )
assume that
A16: x1 in dom (ProjPMap2 (g,t)) and
A17: x2 in dom (ProjPMap2 (g,t)) and
A18: |.(x1 - x2).| < s ; :: thesis: |.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r
A19: Y-section ((dom g),t) = { x where x is Element of REAL : [x,t] in dom g } by MEASUR11:def 5;
A20: ( x1 in Y-section ((dom g),t) & x2 in Y-section ((dom g),t) ) by A16, A17, MESFUN12:def 4;
then A21: ex x being Element of REAL st
( x = x1 & [x,t] in dom g ) by A19;
A22: ex x being Element of REAL st
( x = x2 & [x,t] in dom g ) by A19, A20;
reconsider yy = t as Point of RNS_Real ;
reconsider xx1 = x1 as Point of RNS_Real by XREAL_0:def 1;
reconsider xx2 = x2 as Point of RNS_Real by XREAL_0:def 1;
reconsider p1 = [xx1,yy] as Point of [:RNS_Real,RNS_Real:] ;
reconsider p2 = [xx2,yy] as Point of [:RNS_Real,RNS_Real:] ;
A23: xx1 - xx2 = x1 - x2 by DUALSP03:4;
p1 - p2 = [xx1,yy] + [(- xx2),(- yy)] by PRVECT_3:18;
then p1 - p2 = [(xx1 - xx2),(yy - yy)] by PRVECT_3:18;
then p1 - p2 = [(xx1 - xx2),(0. RNS_Real)] by RLVECT_1:15;
then ||.(p1 - p2).|| = sqrt ((||.(0. RNS_Real).|| ^2) + (||.(xx1 - xx2).|| ^2)) by NDIFF_8:1;
then ||.(p1 - p2).|| = ||.(xx1 - xx2).|| by SQUARE_1:22;
then ||.(p1 - p2).|| = |.(x1 - x2).| by A23, EUCLID:def 2;
then A24: ||.((f /. p1) - (f /. p2)).|| < r by A15, A18, A2, A21, A22;
( (ProjPMap2 (g,t)) . x1 = g . (x1,t) & (ProjPMap2 (g,t)) . x2 = g . (x2,t) ) by A21, A22, MESFUN12:def 4;
then ( (ProjPMap2 (g,t)) . x1 = f /. p1 & (ProjPMap2 (g,t)) . x2 = f /. p2 ) by A2, A21, A22, PARTFUN1:def 6;
then ((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2) = (f /. p1) - (f /. p2) by DUALSP03:4;
hence |.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r by A24, EUCLID:def 2; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom (ProjPMap2 (g,t)) & x2 in dom (ProjPMap2 (g,t)) & |.(x1 - x2).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x2)).| < r ) ) by A14; :: thesis: verum

end;

hence ProjPMap2 (g,t) is uniformly_continuous by FCONT_2:def 1; :: thesis: verum