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 that
A4: 0 <= a and
A5: a < 1 and
A6: 0 < b and
A7: b <= 1 ; :: thesis:

let c be Element of Niemytzki-plane ; :: thesis:
assume c in (+ x,r) " [.0 ,b.[ ; :: thesis:
then A8: (+ x,r) . c in [.0 ,b.[ by FUNCT_1:def 13;
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 A9: z `2 >= 0 by Lm1, Th22;

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

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

reconsider r1 = r * b as real positive number by A6;
reconsider U = (Ball |[x,r1]|,r1) \/ {|[x,0 ]|} as Subset of Niemytzki-plane by Th31;
take U = U; :: thesis:
A11: x is Real by XREAL_0:def 1;
then A12: |[x,0 ]| in y>=0-plane ;
r1 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 A13: U in BB . |[x,0 ]| by A1, A11;
z = |[x,0 ]| by A10, A9, Th64;
hence ( U in Union BB & c in U & U c= (+ x,r) " [.0 ,b.[ ) by A13, A12, A3, A6, Th71, CARD_5:10, SETWISEO:6; :: thesis:

end;

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

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

end;

end;

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) ;
assume c in (+ x,r) " ].a,1.] ; :: thesis:
then A19: (+ x,r) . c in ].a,1.] by FUNCT_1:def 13;
then A20: (+ x,r) . c > a by XXREAL_1:2;
A21: (+ x,r) . c <= 1 by A19, XXREAL_1:2;
A22: z = |[(z `1 ),(z `2 )]| by EUCLID:57;
then A23: z `2 >= 0 by Lm1, Th22;

per cases by A22, A19, A21, Lm1, Th22, XXREAL_0:1, XXREAL_1:2;

suppose z `2 > 0 ; :: thesis:

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

end;

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

then consider r1 being real positive number such that
A29: (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 A22, A28, Th31;
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 A22, A28;
then A30: U in BB . |[(z `1 ),(z `2 )]| by A1, A28;
take U = U; :: thesis:
|[(z `1 ),(z `2 )]| in y>=0-plane by A28;
hence U in Union BB by A30, A3, CARD_5:10; :: thesis:
thus c in U by SETWISEO:6; :: thesis:
1 in ].a,1.] by A5, 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 A29, 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
A31: r1 <= z `2 and
A32: Ball z,r1 c= (+ x,r) " ].a,1.[ by A4, A23, Th69;
reconsider U = Ball z,r1 as Subset of Niemytzki-plane by A22, A31, Th33;
U c= y>=0-plane by A22, A31, Th24;
then A33: U /\ y>=0-plane = U by XBOOLE_1:28;
r1 is Real by XREAL_0:def 1;
then U in { ((Ball |[(z `1 ),(z `2 )]|,q) /\ y>=0-plane ) where q is Element of REAL : q > 0 } by A33, A22;
then A34: U in BB . |[(z `1 ),(z `2 )]| by A31, A2;
take U = U; :: thesis:
|[(z `1 ),(z `2 )]| in y>=0-plane by A31;
hence U in Union BB by A34, 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 A32, Th17, XBOOLE_1:1; :: thesis:

end;

end;

end;

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

end;

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