let f be PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real; :: thesis: for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for x, y being Element of REAL st f is_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is continuous
let g be PartFunc of [:[:REAL,REAL:],REAL:],REAL; :: thesis: for x, y being Element of REAL st f is_continuous_on dom f & f = g holds
ProjPMap1 (g,[x,y]) is continuous
let x, y be Element of REAL ; :: thesis: ( f is_continuous_on dom f & f = g implies ProjPMap1 (g,[x,y]) is continuous )
assume that
A1: f is_continuous_on dom f and
A2: f = g ; :: thesis: ProjPMap1 (g,[x,y]) is continuous
for z0 being Real st z0 in dom (ProjPMap1 (g,[x,y])) holds
ProjPMap1 (g,[x,y]) is_continuous_in z0

proof

let z0 be Real; :: thesis: ( z0 in dom (ProjPMap1 (g,[x,y])) implies ProjPMap1 (g,[x,y]) is_continuous_in z0 )
assume z0 in dom (ProjPMap1 (g,[x,y])) ; :: thesis: ProjPMap1 (g,[x,y]) is_continuous_in z0
then A3: z0 in X-section ((dom g),[x,y]) by MESFUN12:def 3;
A4: X-section ((dom g),[x,y]) = { z where z is Element of REAL : [[x,y],z] in dom g } by MEASUR11:def 4;
then A5: ex z being Element of REAL st
( z = z0 & [[x,y],z] in dom g ) by A3;
reconsider xx = x, yy = y as Point of RNS_Real ;
reconsider zz0 = z0 as Point of RNS_Real by XREAL_0:def 1;
reconsider p0 = [xx,yy,zz0] 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 z1 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for z1 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r ) ) )
assume 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r ) )
then consider s being Real such that
A6: 0 < s and
A7: for p1 being Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] st p1 in dom f & ||.(p1 - p0).|| < s holds
||.((f /. p1) - (f /. p0)).|| < r by A1, A2, A5, NFCONT_1:19;

now :: thesis: for z1 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r

let z1 be Real; :: thesis: ( z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s implies |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r )
assume that
A8: z1 in dom (ProjPMap1 (g,[x,y])) and
A9: |.(z1 - z0).| < s ; :: thesis: |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r
z1 in X-section ((dom g),[x,y]) by A8, MESFUN12:def 3;
then A10: ex z being Element of REAL st
( z = z1 & [[x,y],z] in dom g ) by A4;
reconsider zz1 = z1 as Point of RNS_Real by XREAL_0:def 1;
reconsider p1 = [xx,yy,zz1] as Point of [:[:RNS_Real,RNS_Real:],RNS_Real:] ;
A11: zz1 - zz0 = z1 - z0 by DUALSP03:4;
p1 - p0 = [xx,yy,zz1] + [(- xx),(- yy),(- zz0)] by PRVECT_4:9;
then p1 - p0 = [(xx - xx),(yy - yy),(zz1 - zz0)] by PRVECT_4:9;
then p1 - p0 = [(0. RNS_Real),(yy - yy),(zz1 - zz0)] by RLVECT_1:15;
then p1 - p0 = [(0. RNS_Real),(0. RNS_Real),(zz1 - zz0)] by RLVECT_1:15;
then ||.(p1 - p0).|| = sqrt (((||.(0. RNS_Real).|| ^2) + (||.(0. RNS_Real).|| ^2)) + (||.(zz1 - zz0).|| ^2)) by PRVECT_4:9;
then ||.(p1 - p0).|| = ||.(zz1 - zz0).|| by SQUARE_1:22;
then ||.(p1 - p0).|| = |.(z1 - z0).| by A11, EUCLID:def 2;
then A12: ||.((f /. p1) - (f /. p0)).|| < r by A9, A2, A10, A7;
( (ProjPMap1 (g,[x,y])) . z1 = g . ([x,y],z1) & (ProjPMap1 (g,[x,y])) . z0 = g . ([x,y],z0) ) by A5, A10, MESFUN12:def 3;
then ( (ProjPMap1 (g,[x,y])) . z1 = f /. p1 & (ProjPMap1 (g,[x,y])) . z0 = f /. p0 ) by A2, A5, A10, PARTFUN1:def 6;
then ((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0) = (f /. p1) - (f /. p0) by DUALSP03:4;
hence |.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r by A12, EUCLID:def 2; :: thesis: verum

end;

hence ex s being Real st
( 0 < s & ( for z1 being Real st z1 in dom (ProjPMap1 (g,[x,y])) & |.(z1 - z0).| < s holds
|.(((ProjPMap1 (g,[x,y])) . z1) - ((ProjPMap1 (g,[x,y])) . z0)).| < r ) ) by A6; :: thesis: verum

end;

hence ProjPMap1 (g,[x,y]) is_continuous_in z0 by FCONT_1:3; :: thesis: verum

end;

hence ProjPMap1 (g,[x,y]) is continuous ; :: thesis: verum