let X, Y be RealNormSpace; :: thesis: for V being Subset of [:X,Y:] holds

( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

let V be Subset of [:X,Y:]; :: thesis: ( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ; :: thesis: V is open

for z being Point of [:X,Y:] st z in V holds

ex s being Real st

( s > 0 & Ball (z,s) c= V )

( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

let V be Subset of [:X,Y:]; :: thesis: ( V is open iff for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

hereby :: thesis: ( ( for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ) implies V is open )

assume A3:
for x being Point of Xfor y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ) implies V is open )

assume A1:
V is open
; :: thesis: for x being Point of X

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

let x be Point of X; :: thesis: for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

let y be Point of Y; :: thesis: ( [x,y] in V implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

assume [x,y] in V ; :: thesis: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

then consider r being Real such that

A2: ( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V ) by A1, NDIFF_8:23;

thus ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A2; :: thesis: verum

end;for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

let x be Point of X; :: thesis: for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

let y be Point of Y; :: thesis: ( [x,y] in V implies ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

assume [x,y] in V ; :: thesis: ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )

then consider r being Real such that

A2: ( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V ) by A1, NDIFF_8:23;

thus ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A2; :: thesis: verum

for y being Point of Y st [x,y] in V holds

ex r1, r2 being Real st

( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ; :: thesis: V is open

for z being Point of [:X,Y:] st z in V holds

ex s being Real st

( s > 0 & Ball (z,s) c= V )

proof

hence
V is open
by NDIFF_8:20; :: thesis: verum
let z be Point of [:X,Y:]; :: thesis: ( z in V implies ex s being Real st

( s > 0 & Ball (z,s) c= V ) )

assume A4: z in V ; :: thesis: ex s being Real st

( s > 0 & Ball (z,s) c= V )

consider x being Point of X, y being Point of Y such that

A5: z = [x,y] by PRVECT_3:18;

consider r1, r2 being Real such that

A6: ( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A3, A4, A5;

consider s being Real such that

A7: ( s = min (r1,r2) & s > 0 ) and

A8: Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] by A5, A6, Th2;

take s ; :: thesis: ( s > 0 & Ball (z,s) c= V )

thus ( s > 0 & Ball (z,s) c= V ) by A6, A7, A8, XBOOLE_1:1; :: thesis: verum

end;( s > 0 & Ball (z,s) c= V ) )

assume A4: z in V ; :: thesis: ex s being Real st

( s > 0 & Ball (z,s) c= V )

consider x being Point of X, y being Point of Y such that

A5: z = [x,y] by PRVECT_3:18;

consider r1, r2 being Real such that

A6: ( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A3, A4, A5;

consider s being Real such that

A7: ( s = min (r1,r2) & s > 0 ) and

A8: Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] by A5, A6, Th2;

take s ; :: thesis: ( s > 0 & Ball (z,s) c= V )

thus ( s > 0 & Ball (z,s) c= V ) by A6, A7, A8, XBOOLE_1:1; :: thesis: verum