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_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_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_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_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_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) holds
p2 is_continuous_on dom p2
let z be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g & p2 = ProjPMap2 (g,z) implies p2 is_continuous_on dom p2 )
assume that
A1: f is_continuous_on dom f and
A2: f = g and
A3: p2 = ProjPMap2 (g,z) ; :: thesis: p2 is_continuous_on dom p2
for xy0 being Point of [:RNS_Real,RNS_Real:] st xy0 in dom p2 holds
p2 | (dom p2) is_continuous_in xy0

proof

let xy0 be Point of [:RNS_Real,RNS_Real:]; :: thesis: ( xy0 in dom p2 implies p2 | (dom p2) is_continuous_in xy0 )
assume A4: xy0 in dom p2 ; :: thesis: p2 | (dom p2) is_continuous_in xy0
then A5: xy0 in Y-section ((dom g),z) by A3, MESFUN12:def 4;
A6: Y-section ((dom g),z) = { t where t is Element of [:RNS_Real,RNS_Real:] : [t,z] in dom g } by MEASUR11:def 5;
then consider t being Element of [:RNS_Real,RNS_Real:] such that
A7: ( t = xy0 & [t,z] in dom g ) by A5;
consider xx0, yy0 being Point of RNS_Real such that
A8: xy0 = [xx0,yy0] by PRVECT_3:18;
reconsider x0 = xx0, y0 = yy0 as Real ;
reconsider zz = z as Point of RNS_Real ;
reconsider v0 = [xx0,yy0,zz] as Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] ;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for xy1 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom (p2 | (dom p2)) & ||.(xy1 - xy0).|| < s holds
||.((p2 /. xy1) - (p2 /. xy0)).|| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for xy1 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom (p2 | (dom p2)) & ||.(xy1 - xy0).|| < s holds
||.((p2 /. xy1) - (p2 /. xy0)).|| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for xy1 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom (p2 | (dom p2)) & ||.(xy1 - xy0).|| < s holds
||.((p2 /. xy1) - (p2 /. xy0)).|| < r ) )
then consider s being Real such that
A9: 0 < s and
A10: for v1 being Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] st v1 in dom f & ||.(v1 - v0).|| < s holds
||.((f /. v1) - (f /. v0)).|| < r by A1, A2, A7, A8, NFCONT_1:19;

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

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

end;

hence ex s being Real st
( 0 < s & ( for xy1 being Point of [:RNS_Real,RNS_Real:] st xy1 in dom (p2 | (dom p2)) & ||.(xy1 - xy0).|| < s holds
||.((p2 /. xy1) - (p2 /. xy0)).|| < r ) ) by A9; :: thesis: verum

end;

hence p2 | (dom p2) is_continuous_in xy0 by A4, NFCONT_1:7; :: thesis: verum

end;

hence p2 is_continuous_on dom p2 ; :: thesis: verum