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 P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for s being Element of REAL st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,s) holds
P2 is_uniformly_continuous_on dom P2
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 P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for s being Element of REAL st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,s) holds
P2 is_uniformly_continuous_on dom P2
let g be PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL; :: thesis: for P2 being PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real
for s being Element of REAL st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,s) holds
P2 is_uniformly_continuous_on dom P2
let P2 be PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real; :: thesis: for s being Element of REAL st f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,s) holds
P2 is_uniformly_continuous_on dom P2
let q be Element of REAL ; :: thesis: ( f is_uniformly_continuous_on dom f & f = g & P2 = ProjPMap2 (g,q) 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,q) ; :: thesis: P2 is_uniformly_continuous_on dom P2
for r being Real st 0 < r holds
ex s0 being Real st
( 0 < s0 & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 holds
||.((P2 /. x1) - (P2 /. x2)).|| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s0 being Real st
( 0 < s0 & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 holds
||.((P2 /. x1) - (P2 /. x2)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s0 being Real st
( 0 < s0 & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 holds
||.((P2 /. x1) - (P2 /. x2)).|| < r ) )
then consider s0 being Real such that
A4: 0 < s0 and
A5: for p1, p2 being Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] st p1 in dom f & p2 in dom f & ||.(p1 - p2).|| < s0 holds
||.((f /. p1) - (f /. p2)).|| < r by A1;

now :: thesis: for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 holds
||.((P2 /. x1) - (P2 /. x2)).|| < r

let x1, x2 be Point of (CarProduct ((Seg n) --> RNS_Real)); :: thesis: ( x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 implies ||.((P2 /. x1) - (P2 /. x2)).|| < r )
assume that
A6: x1 in dom P2 and
A7: x2 in dom P2 and
A8: ||.(x1 - x2).|| < s0 ; :: thesis: ||.((P2 /. x1) - (P2 /. x2)).|| < r
A9: Y-section ((dom g),q) = { x where x is Element of CarProduct ((Seg n) --> REAL) : [x,q] in dom g } by MEASUR11:def 5;
A10: ( x1 in Y-section ((dom g),q) & x2 in Y-section ((dom g),q) ) by A3, A6, A7, MESFUN12:def 4;
then A11: ex x being Element of CarProduct ((Seg n) --> REAL) st
( x = x1 & [x,q] in dom g ) by A9;
A12: ex x being Element of CarProduct ((Seg n) --> REAL) st
( x = x2 & [x,q] in dom g ) by A9, A10;
reconsider yy = q as Point of RNS_Real ;
reconsider p1 = [x1,yy], p2 = [x2,yy] as Point of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:] ;
p1 - p2 = [x1,yy] + [(- x2),(- yy)] by PRVECT_3:18;
then p1 - p2 = [(x1 - x2),(yy - yy)] by PRVECT_3:18;
then p1 - p2 = [(x1 - x2),(0. RNS_Real)] by RLVECT_1:15;
then ||.(p1 - p2).|| = sqrt ((||.(0. RNS_Real).|| ^2) + (||.(x1 - x2).|| ^2)) by NDIFF_8:1;
then A13: ||.(p1 - p2).|| = ||.(x1 - x2).|| by SQUARE_1:22;
( (ProjPMap2 (g,q)) . x1 = g . (x1,q) & (ProjPMap2 (g,q)) . x2 = g . (x2,q) ) by A11, A12, MESFUN12:def 4;
then ( P2 /. x1 = g . (x1,q) & P2 /. x2 = g . (x2,q) ) by A3, A6, A7, PARTFUN1:def 6;
then ( P2 /. x1 = f /. p1 & P2 /. x2 = f /. p2 ) by A2, A11, A12, PARTFUN1:def 6;
hence ||.((P2 /. x1) - (P2 /. x2)).|| < r by A5, A8, A2, A11, A12, A13; :: thesis: verum

end;

hence ex s0 being Real st
( 0 < s0 & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st x1 in dom P2 & x2 in dom P2 & ||.(x1 - x2).|| < s0 holds
||.((P2 /. x1) - (P2 /. x2)).|| < r ) ) by A4; :: thesis: verum

end;

hence P2 is_uniformly_continuous_on dom P2 ; :: thesis: verum