set f = + (x,y,r);
consider BB being Neighborhood_System of Niemytzki-plane such that
A1:
for x being Real holds BB . |[x,0]| = { ((Ball (|[x,q]|,q)) \/ {|[x,0]|}) where q is Real : q > 0 }
and
A2:
for x, y being Real st y > 0 holds
BB . |[x,y]| = { ((Ball (|[x,y]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by Def3;
A3:
dom BB = y>=0-plane
by Lm1, PARTFUN1:def 2;
now for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds
( (+ (x,y,r)) " [.0,b.[ is open & (+ (x,y,r)) " ].a,1.] is open )let a,
b be
Real;
( 0 <= a & a < 1 & 0 < b & b <= 1 implies ( (+ (x,y,r)) " [.0,b.[ is open & (+ (x,y,r)) " ].a,1.] is open ) )assume that A4:
0 <= a
and
a < 1
and A5:
0 < b
and A6:
b <= 1
;
( (+ (x,y,r)) " [.0,b.[ is open & (+ (x,y,r)) " ].a,1.] is open )
(+ (x,y,r)) " [.0,b.[ = (Ball (|[x,y]|,(r * b))) /\ y>=0-plane
by A5, A6, Th78;
hence
(+ (x,y,r)) " [.0,b.[ is
open
by A5, Th28;
(+ (x,y,r)) " ].a,1.] is open now for c being Element of Niemytzki-plane st c in (+ (x,y,r)) " ].a,1.] holds
ex U being Subset of Niemytzki-plane st
( U in Union BB & c in U & U c= (+ (x,y,r)) " ].a,1.] )let c be
Element of
Niemytzki-plane;
( c in (+ (x,y,r)) " ].a,1.] implies ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,y,r)) " ].a,1.] ) )
c in y>=0-plane
by Lm1;
then reconsider z =
c as
Point of
(TOP-REAL 2) ;
A7:
z = |[(z `1),(z `2)]|
by EUCLID:53;
assume
c in (+ (x,y,r)) " ].a,1.]
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,y,r)) " ].a,1.] )then
(+ (x,y,r)) . c in ].a,1.]
by FUNCT_1:def 7;
then A8:
(+ (x,y,r)) . c > a
by XXREAL_1:2;
per cases
( z `2 > 0 or z `2 = 0 )
by A7, Lm1, Th18;
suppose A9:
z `2 > 0
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,y,r)) " ].a,1.] )then reconsider r1 =
|.(|[x,y]| - z).| - (r * a) as
positive Real by A4, A8, Th79, XREAL_1:50;
reconsider U =
(Ball (z,r1)) /\ y>=0-plane as
Subset of
Niemytzki-plane by A7, A9, Th28;
U in { ((Ball (|[(z `1),(z `2)]|,q)) /\ y>=0-plane) where q is Real : q > 0 }
by A7;
then A10:
U in BB . |[(z `1),(z `2)]|
by A2, A9;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,y,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane
by A9;
hence
U in Union BB
by A10, A3, CARD_5:2;
( c in U & U c= (+ (x,y,r)) " ].a,1.] )
c in Ball (
z,
r1)
by Th13;
hence
(
c in U &
U c= (+ (x,y,r)) " ].a,1.] )
by A4, A8, A9, Lm1, Th79, XBOOLE_0:def 4;
verum end; suppose A11:
z `2 = 0
;
ex U being Subset of Niemytzki-plane st
( b2 in Union BB & U in b2 & b2 c= (+ (x,y,r)) " ].a,1.] )then consider r1 being
positive Real such that
r1 = (|.(|[x,y]| - z).| - (r * a)) / 2
and A12:
(Ball (|[(z `1),r1]|,r1)) \/ {z} c= (+ (x,y,r)) " ].a,1.]
by A4, A8, Th80;
reconsider U =
(Ball (|[(z `1),r1]|,r1)) \/ {z} as
Subset of
Niemytzki-plane by A7, A11, Th27;
U in { ((Ball (|[(z `1),q]|,q)) \/ {|[(z `1),0]|}) where q is Real : q > 0 }
by A7, A11;
then A13:
U in BB . |[(z `1),(z `2)]|
by A1, A11;
take U =
U;
( U in Union BB & c in U & U c= (+ (x,y,r)) " ].a,1.] )
|[(z `1),(z `2)]| in y>=0-plane
by A11;
hence
U in Union BB
by A13, A3, CARD_5:2;
( c in U & U c= (+ (x,y,r)) " ].a,1.] )thus
c in U
by ZFMISC_1:136;
U c= (+ (x,y,r)) " ].a,1.]thus
U c= (+ (x,y,r)) " ].a,1.]
by A12;
verum end; end; hence
(+ (x,y,r)) " ].a,1.] is
open
by YELLOW_9:31;
verum end;
hence
+ (x,y,r) is continuous
by Th75; verum