let n be non zero Nat; :: 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
for p being Element of CarProduct ((Seg n) --> REAL) st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,p) is uniformly_continuous
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
for p being Element of CarProduct ((Seg n) --> REAL) st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,p) is uniformly_continuous
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for p being Element of CarProduct ((Seg n) --> REAL) st f is_uniformly_continuous_on dom f & f = g holds
ProjPMap1 (g,p) is uniformly_continuous
let p be Element of CarProduct ((Seg n) --> REAL); :: thesis: ( f is_uniformly_continuous_on dom f & f = g implies ProjPMap1 (g,p) is uniformly_continuous )
assume that
A1: f is_uniformly_continuous_on dom f and
A2: f = g ; :: thesis: ProjPMap1 (g,p) is uniformly_continuous
set P1 = ProjPMap1 (g,p);
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,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . 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,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y1, y2 being Real st y1 in dom (ProjPMap1 (g,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r ) )
then consider s being Real such that
A3: 0 < s and
A4: for p1, p2 being Point of [:(CarProduct ((Seg n) --> 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,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r

let y1, y2 be Real; :: thesis: ( y1 in dom (ProjPMap1 (g,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s implies |.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r )
assume that
A5: y1 in dom (ProjPMap1 (g,p)) and
A6: y2 in dom (ProjPMap1 (g,p)) and
A7: |.(y1 - y2).| < s ; :: thesis: |.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r
A8: X-section ((dom g),p) = { y where y is Element of REAL : [p,y] in dom g } by MEASUR11:def 4;
A9: ( y1 in X-section ((dom g),p) & y2 in X-section ((dom g),p) ) by A5, A6, MESFUN12:def 3;
then A10: ex y being Element of REAL st
( y = y1 & [p,y] in dom g ) by A8;
A11: ex y being Element of REAL st
( y = y2 & [p,y] in dom g ) by A8, A9;
reconsider xx = p as Point of (CarProduct ((Seg n) --> RNS_Real)) by MEASUR15:42;
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], p2 = [xx,yy2] as Point of [:(CarProduct ((Seg n) --> 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. (CarProduct ((Seg n) --> RNS_Real))),(yy1 - yy2)] by RLVECT_1:15;
then ||.(p1 - p2).|| = sqrt ((||.(0. (CarProduct ((Seg n) --> 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,p)) . y1 = g . (p,y1) & (ProjPMap1 (g,p)) . y2 = g . (p,y2) ) by A10, A11, MESFUN12:def 3;
then ( (ProjPMap1 (g,p)) . y1 = f /. p1 & (ProjPMap1 (g,p)) . y2 = f /. p2 ) by A2, A10, A11, PARTFUN1:def 6;
then ((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2) = (f /. p1) - (f /. p2) by DUALSP03:4;
hence |.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . 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,p)) & y2 in dom (ProjPMap1 (g,p)) & |.(y1 - y2).| < s holds
|.(((ProjPMap1 (g,p)) . y1) - ((ProjPMap1 (g,p)) . y2)).| < r ) ) by A3; :: thesis: verum

end;

hence ProjPMap1 (g,p) is uniformly_continuous by FCONT_2:def 1; :: thesis: verum