set f = + x,r;
consider BB being Neighborhood_System of Niemytzki-plane such that
A1: for x being Element of REAL holds BB . |[x,0 ]| = { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 } and
A2: for x, y being Element of REAL st y > 0 holds
BB . |[x,y]| = { ((Ball |[x,y]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } by Def3;
A3: dom BB = y>=0-plane by Lm1, PARTFUN1:def 4;

let a, b be real number ; :: thesis:
assume A4: ( 0 <= a & a < 1 & 0 < b & b <= 1 ) ; :: thesis:

let c be Element of Niemytzki-plane ; :: thesis:
c in y>=0-plane by Lm1;
then reconsider z = c as Point of (TOP-REAL 2) ;
z = |[(z `1 ),(z `2 )]| by EUCLID:57;
then A5: z `2 >= 0 by Lm1, Th22;
assume c in (+ x,r) " [.0 ,b.[ ; :: thesis:
then A6: (+ x,r) . c in [.0 ,b.[ by FUNCT_1:def 13;

per cases ) . c = 0 or ( 0 < (+ x,r) . c & (+ x,r) . c < b ) ) by A6, XXREAL_1:3;

suppose (+ x,r) . c = 0 ; :: thesis:

then A7: ( z = |[x,0 ]| & 0 < b ) by A4, A5, Th64;
r * b > 0 * b by A4;
then reconsider r1 = r * b as real positive number ;
reconsider U = (Ball |[x,r1]|,r1) \/ {|[x,0 ]|} as Subset of Niemytzki-plane by Th31;
take U = U; :: thesis:
A8: ( r1 is Real & x is Real ) by XREAL_0:def 1;
then U in { ((Ball |[x,q]|,q) \/ {|[x,0 ]|}) where q is Element of REAL : q > 0 } ;
then ( U in BB . |[x,0 ]| & |[x,0 ]| in y>=0-plane ) by A1, A8;
hence ( U in Union BB & c in U & U c= (+ x,r) " [.0 ,b.[ ) by A3, A7, Th71, CARD_5:10, SETWISEO:6; :: thesis:

end;

suppose ( 0 < (+ x,r) . c & (+ x,r) . c < b ) ; :: thesis:

then A9: ( z in Ball |[x,(r * b)]|,(r * b) & Ball |[x,(r * b)]|,(r * b) c= (+ x,r) " ].0 ,b.[ & 0 < b ) by A4, A5, Th70, Th72;
r * b > 0 * b by A4;
then reconsider r1 = r * b as real positive number ;
reconsider U = Ball |[x,r1]|,r1 as Subset of Niemytzki-plane by Th33;
take U = U; :: thesis:
U c= y>=0-plane by Th24;
then A10: ( U /\ y>=0-plane = U & r1 is Real & x is Real ) by XBOOLE_1:28, XREAL_0:def 1;
then U in { ((Ball |[x,r1]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } ;
then ( U in BB . |[x,r1]| & |[x,r1]| in y>=0-plane ) by A2, A10;
hence U in Union BB by A3, CARD_5:10; :: thesis:
(+ x,r) " ].0 ,b.[ c= (+ x,r) " [.0 ,b.[ by RELAT_1:178, XXREAL_1:45;
hence ( c in U & U c= (+ x,r) " [.0 ,b.[ ) by A9, XBOOLE_1:1; :: thesis:

end;

hence (+ x,r) " [.0 ,b.[ is open by YELLOW_9:31; :: thesis:

let c be Element of Niemytzki-plane ; :: thesis:
c in y>=0-plane by Lm1;
then reconsider z = c as Point of (TOP-REAL 2) ;
A11: z = |[(z `1 ),(z `2 )]| by EUCLID:57;
then A12: z `2 >= 0 by Lm1, Th22;
assume c in (+ x,r) " ].a,1.] ; :: thesis:
then (+ x,r) . c in ].a,1.] by FUNCT_1:def 13;
then A13: ( (+ x,r) . c > a & (+ x,r) . c <= 1 ) by XXREAL_1:2;

per cases by A11, A13, Lm1, Th22, XXREAL_0:1;

suppose z `2 > 0 ; :: thesis:

then consider r1 being real positive number such that
A14: ( r1 <= z `2 & Ball z,r1 c= (+ x,r) " ].a,1.] ) by A4, A13, Th73;
reconsider U = Ball z,r1 as Subset of Niemytzki-plane by A11, A14, Th33;
take U = U; :: thesis:
U c= y>=0-plane by A11, A14, Th24;
then ( U /\ y>=0-plane = U & r1 is Real & x is Real ) by XBOOLE_1:28, XREAL_0:def 1;
then ( U in { ((Ball |[(z `1 ),(z `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } & z `2 > 0 ) by A11, A14;
then ( U in BB . |[(z `1 ),(z `2 )]| & |[(z `1 ),(z `2 )]| in y>=0-plane ) by A2;
hence U in Union BB by A3, CARD_5:10; :: thesis:
thus ( c in U & U c= (+ x,r) " ].a,1.] ) by A14, Th17; :: thesis:

end;

suppose A15: ( (+ x,r) . c = 1 & z `2 = 0 ) ; :: thesis:

then consider r1 being real positive number such that
A16: (Ball |[(z `1 ),r1]|,r1) \/ {z} c= (+ x,r) " {1} by Th74;
reconsider U = (Ball |[(z `1 ),r1]|,r1) \/ {z} as Subset of Niemytzki-plane by A11, A15, Th31;
take U = U; :: thesis:
r1 is Real by XREAL_0:def 1;
then U in { ((Ball |[(z `1 ),q]|,q) \/ {|[(z `1 ),0 ]|}) where q is Element of REAL : q > 0 } by A11, A15;
then ( U in BB . |[(z `1 ),(z `2 )]| & |[(z `1 ),(z `2 )]| in y>=0-plane ) by A1, A15;
hence U in Union BB by A3, CARD_5:10; :: thesis:
thus c in U by SETWISEO:6; :: thesis:
1 in ].a,1.] by A4, XXREAL_1:2;
then {1} c= ].a,1.] by ZFMISC_1:37;
then (+ x,r) " {1} c= (+ x,r) " ].a,1.] by RELAT_1:178;
hence U c= (+ x,r) " ].a,1.] by A16, XBOOLE_1:1; :: thesis:

end;

suppose ( a < (+ x,r) . c & (+ x,r) . c < 1 ) ; :: thesis:

then (+ x,r) . c in ].a,1.[ by XXREAL_1:4;
then consider r1 being real positive number such that
A17: ( r1 <= z `2 & Ball z,r1 c= (+ x,r) " ].a,1.[ ) by A4, A12, Th69;
reconsider U = Ball z,r1 as Subset of Niemytzki-plane by A11, A17, Th33;
take U = U; :: thesis:
U c= y>=0-plane by A11, A17, Th24;
then ( U /\ y>=0-plane = U & r1 is Real & x is Real ) by XBOOLE_1:28, XREAL_0:def 1;
then ( U in { ((Ball |[(z `1 ),(z `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } & z `2 > 0 ) by A11, A17;
then ( U in BB . |[(z `1 ),(z `2 )]| & |[(z `1 ),(z `2 )]| in y>=0-plane ) by A2;
hence U in Union BB by A3, CARD_5:10; :: thesis:
(+ x,r) " ].a,1.[ c= (+ x,r) " ].a,1.] by RELAT_1:178, XXREAL_1:41;
hence ( c in U & U c= (+ x,r) " ].a,1.] ) by A17, Th17, XBOOLE_1:1; :: thesis:

end;

hence (+ x,r) " ].a,1.] is open by YELLOW_9:31; :: thesis:

end;

hence + x,r is continuous by Th79; :: thesis: