let f be PartFunc of [:RNS_Real,RNS_Real:],RNS_Real; :: thesis:
let g be PartFunc of [:REAL,REAL:],REAL; :: thesis:
let t be Element of REAL ; :: thesis:
assume that
A1: f is_continuous_on dom f and
A2: f = g ; :: thesis:
for y0 being Real st y0 in dom (ProjPMap1 (g,t)) holds
ProjPMap1 (g,t) is_continuous_in y0

let y0 be Real; :: thesis:
assume y0 in dom (ProjPMap1 (g,t)) ; :: thesis:
then A3: y0 in X-section ((dom g),t) by MESFUN12:def 3;
A4: X-section ((dom g),t) = { y where y is Element of REAL : [t,y] in dom g } by MEASUR11:def 4;
then A5: ex y being Element of REAL st
( y = y0 & [t,y] in dom g ) by A3;
reconsider xx = t as Point of RNS_Real ;
reconsider yy0 = y0 as Point of RNS_Real by XREAL_0:def 1;
reconsider p0 = [xx,yy0] as Point of [:RNS_Real,RNS_Real:] ;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Real st y1 in dom (ProjPMap1 (g,t)) & |.(y1 - y0).| < s holds
|.(((ProjPMap1 (g,t)) . y1) - ((ProjPMap1 (g,t)) . y0)).| < r ) )

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A6: 0 < s and
A7: for p1 being Point of [: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;

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

end;

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

end;

hence ProjPMap1 (g,t) is_continuous_in y0 by FCONT_1:3; :: thesis:

end;

hence ProjPMap1 (g,t) is continuous ; :: thesis:
for x0 being Real st x0 in dom (ProjPMap2 (g,t)) holds
ProjPMap2 (g,t) is_continuous_in x0

let x0 be Real; :: thesis:
assume x0 in dom (ProjPMap2 (g,t)) ; :: thesis:
then A13: x0 in Y-section ((dom g),t) by MESFUN12:def 4;
A14: Y-section ((dom g),t) = { x where x is Element of REAL : [x,t] in dom g } by MEASUR11:def 5;
then A15: ex x being Element of REAL st
( x = x0 & [x,t] in dom g ) by A13;
reconsider yy = t as Point of RNS_Real ;
reconsider xx0 = x0 as Point of RNS_Real by XREAL_0:def 1;
reconsider p0 = [xx0,yy] as Point of [:RNS_Real,RNS_Real:] ;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom (ProjPMap2 (g,t)) & |.(x1 - x0).| < s holds
|.(((ProjPMap2 (g,t)) . x1) - ((ProjPMap2 (g,t)) . x0)).| < r ) )

let r be Real; :: thesis:
assume 0 < r ; :: thesis:
then consider s being Real such that
A16: 0 < s and
A17: for p1 being Point of [:RNS_Real,RNS_Real:] st p1 in dom f & ||.(p1 - p0).|| < s holds
||.((f /. p1) - (f /. p0)).|| < r by A1, A2, A15, NFCONT_1:19;

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

end;

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

end;

hence ProjPMap2 (g,t) is_continuous_in x0 by FCONT_1:3; :: thesis:

end;

hence ProjPMap2 (g,t) is continuous ; :: thesis: