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

for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

let V be Subset of [:X,Y:]; :: thesis: for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

let D be Subset of X; :: thesis: ( D is open & V = [:D, the carrier of Y:] implies V is open )

assume A1: ( D is open & V = [:D, the carrier of Y:] ) ; :: thesis: V is open

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 D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

let V be Subset of [:X,Y:]; :: thesis: for D being Subset of X st D is open & V = [:D, the carrier of Y:] holds

V is open

let D be Subset of X; :: thesis: ( D is open & V = [:D, the carrier of Y:] implies V is open )

assume A1: ( D is open & V = [:D, the carrier of Y:] ) ; :: thesis: V is open

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 )

proof

hence
V is open
by Th3; :: thesis: verum
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 ( x in D & y in the carrier of Y ) by A1, ZFMISC_1:87;

then consider r being Real such that

A2: ( r > 0 & Ball (x,r) c= D ) by A1, NDIFF_8:20;

[:(Ball (x,r)),(Ball (y,r)):] c= V

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

end;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 ( x in D & y in the carrier of Y ) by A1, ZFMISC_1:87;

then consider r being Real such that

A2: ( r > 0 & Ball (x,r) c= D ) by A1, NDIFF_8:20;

[:(Ball (x,r)),(Ball (y,r)):] c= V

proof

hence
ex r1, r2 being Real st
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(Ball (x,r)),(Ball (y,r)):] or z in V )

assume z in [:(Ball (x,r)),(Ball (y,r)):] ; :: thesis: z in V

then consider qx, qy being object such that

A4: ( qx in Ball (x,r) & qy in Ball (y,r) & z = [qx,qy] ) by ZFMISC_1:def 2;

thus z in V by A1, A2, A4, ZFMISC_1:87; :: thesis: verum

end;assume z in [:(Ball (x,r)),(Ball (y,r)):] ; :: thesis: z in V

then consider qx, qy being object such that

A4: ( qx in Ball (x,r) & qy in Ball (y,r) & z = [qx,qy] ) by ZFMISC_1:def 2;

thus z in V by A1, A2, A4, ZFMISC_1:87; :: thesis: verum

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