let n, k be Nat; :: thesis: for Ak being Subset of ()
for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of () : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )

let Ak be Subset of (); :: thesis: for A being Subset of (TOP-REAL (k + n)) st A = { (v ^ (n |-> 0)) where v is Element of () : verum } holds
for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )

set kn = k + n;
set TRn = TOP-REAL (k + n);
set TRk = TOP-REAL k;
let A be Subset of (TOP-REAL (k + n)); :: thesis: ( A = { (v ^ (n |-> 0)) where v is Element of () : verum } implies for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open ) )

assume A1: A = { (v ^ (n |-> 0)) where v is Element of () : verum } ; :: thesis: for B being Subset of ((TOP-REAL (k + n)) | A) st B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } holds
( Ak is open iff B is open )

A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider p = Ak as Subset of () ;
set TRA = (TOP-REAL (k + n)) | A;
let B be Subset of ((TOP-REAL (k + n)) | A); :: thesis: ( B = { v where v is Point of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } implies ( Ak is open iff B is open ) )
assume A3: B = { v where v is Element of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } ; :: thesis: ( Ak is open iff B is open )
A4: [#] ((TOP-REAL (k + n)) | A) = A by PRE_TOPC:def 5;
A5: k + n >= k by NAT_1:11;
hereby :: thesis: ( B is open implies Ak is open )
set PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ;
{ v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } c= [#] (TOP-REAL (k + n))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } or x in [#] (TOP-REAL (k + n)) )
assume x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ; :: thesis: x in [#] (TOP-REAL (k + n))
then ex v being Element of (TOP-REAL (k + n)) st
( x = v & v | k in Ak ) ;
hence x in [#] (TOP-REAL (k + n)) ; :: thesis: verum
end;
then reconsider PP = { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } as Subset of (TOP-REAL (k + n)) ;
A6: PP /\ A c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PP /\ A or x in B )
assume A7: x in PP /\ A ; :: thesis: x in B
then x in PP by XBOOLE_0:def 4;
then consider v being Element of (TOP-REAL (k + n)) such that
A8: ( x = v & v | k in Ak ) ;
x in A by ;
hence x in B by A3, A8; :: thesis: verum
end;
assume Ak is open ; :: thesis: B is open
then PP is open by ;
then PP in the topology of (TOP-REAL (k + n)) by PRE_TOPC:def 2;
then A9: PP /\ ([#] ((TOP-REAL (k + n)) | A)) in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def 4;
B c= PP /\ A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in PP /\ A )
assume x in B ; :: thesis: x in PP /\ A
then consider v being Element of (TOP-REAL (k + n)) such that
A10: x = v and
A11: v | k in Ak and
A12: v in A by A3;
v in PP by A11;
hence x in PP /\ A by ; :: thesis: verum
end;
then B = PP /\ A by A6;
hence B is open by ; :: thesis: verum
end;
assume B is open ; :: thesis: Ak is open
then B in the topology of ((TOP-REAL (k + n)) | A) by PRE_TOPC:def 2;
then consider Q being Subset of (TOP-REAL (k + n)) such that
A13: Q in the topology of (TOP-REAL (k + n)) and
A14: Q /\ ([#] ((TOP-REAL (k + n)) | A)) = B by PRE_TOPC:def 4;
A15: TopStruct(# the carrier of (TOP-REAL (k + n)), the topology of (TOP-REAL (k + n)) #) = TopSpaceMetr (Euclid (k + n)) by EUCLID:def 8;
then reconsider q = Q as Subset of (TopSpaceMetr (Euclid (k + n))) ;
A16: q is open by ;
for e being Point of () st e in p holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p )
proof
let e be Point of (); :: thesis: ( e in p implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p ) )

A17: len (n |-> 0) = n by CARD_1:def 7;
A18: @ (@ (e ^ (n |-> 0))) = e ^ (n |-> 0) ;
A19: len e = k by CARD_1:def 7;
then len (e ^ (n |-> 0)) = k + n by ;
then reconsider e0 = e ^ (n |-> 0) as Point of (Euclid (k + n)) by ;
dom e = Seg k by ;
then A20: e = e0 | k by FINSEQ_1:21;
n |-> 0 = @ (@ (n |-> 0)) ;
then reconsider N = n |-> 0 as Element of () by ;
e is Element of () by Lm1;
then A21: e0 in A by A1;
assume e in p ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p )

then e0 in B by A3, A21, A20;
then e0 in q by ;
then consider m being non zero Element of NAT such that
A22: OpenHypercube (e0,(1 / m)) c= q by ;
set r = 1 / m;
take 1 / m ; :: thesis: ( 1 / m > 0 & OpenHypercube (e,(1 / m)) c= p )
thus 1 / m > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,(1 / m)) c= p
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in OpenHypercube (e,(1 / m)) or x in p )
N in OpenHypercube (N,(1 / m)) by ;
then A23: N in product (Intervals (N,(1 / m))) by EUCLID_9:def 4;
assume A24: x in OpenHypercube (e,(1 / m)) ; :: thesis: x in p
then reconsider w = x as Point of () by A2;
A25: (Intervals (e,(1 / m))) ^ (Intervals (N,(1 / m))) = Intervals ((e ^ N),(1 / m)) by Th1;
w in product (Intervals (e,(1 / m))) by ;
then w ^ N in product (Intervals (e0,(1 / m))) by ;
then A26: w ^ N in OpenHypercube (e0,(1 / m)) by EUCLID_9:def 4;
w ^ N in A by A1;
then w ^ N in B by ;
then A27: ex v being Element of (TOP-REAL (k + n)) st
( w ^ N = v & v | k in Ak & v in A ) by A3;
len w = k by CARD_1:def 7;
then (w ^ N) | k = (w ^ N) | (dom w) by FINSEQ_1:def 3
.= w by FINSEQ_1:21 ;
hence x in p by A27; :: thesis: verum
end;
then p is open by EUCLID_9:24;
then Ak in the topology of () by ;
hence Ak is open by PRE_TOPC:def 2; :: thesis: verum