let n, k be Nat; :: thesis:
let Ak be Subset of (TOP-REAL k); :: thesis:
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:
assume A1: A = { (v ^ (n |-> 0)) where v is Element of (TOP-REAL k) : verum } ; :: thesis:
A2: TopStruct(# the carrier of (TOP-REAL k), the topology of (TOP-REAL k) #) = TopSpaceMetr (Euclid k) by EUCLID:def 8;
then reconsider p = Ak as Subset of (TopSpaceMetr (Euclid k)) ;
set TRA = (TOP-REAL (k + n)) | A;
let B be Subset of ((TOP-REAL (k + n)) | A); :: thesis:
assume A3: B = { v where v is Element of (TOP-REAL (k + n)) : ( v | k in Ak & v in A ) } ; :: thesis:
A4: [#] ((TOP-REAL (k + n)) | A) = A by PRE_TOPC:def 5;
A5: k + n >= k by NAT_1:11;

hereby :: thesis:

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:
assume x in { v where v is Element of (TOP-REAL (k + n)) : v | k in Ak } ; :: thesis:
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:

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:
assume A7: x in PP /\ A ; :: thesis:
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 A7, XBOOLE_0:def 4;
hence x in B by A3, A8; :: thesis:

end;

assume Ak is open ; :: thesis:
then PP is open by A5, Th7;
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:
assume x in B ; :: thesis:
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 A10, A12, XBOOLE_0:def 4; :: thesis:

end;

then B = PP /\ A by A6;
hence B is open by A4, A9, PRE_TOPC:def 2; :: thesis:

end;

assume B is open ; :: thesis:
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 A13, A15, PRE_TOPC:def 2;
for e being Point of (Euclid k) st e in p holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= p )

proof

let e be Point of (Euclid k); :: thesis:
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 A17, FINSEQ_1:22;
then reconsider e0 = e ^ (n |-> 0) as Point of (Euclid (k + n)) by A18, TOPREAL3:45;
dom e = Seg k by A19, FINSEQ_1:def 3;
then A20: e = e0 | k by FINSEQ_1:21;
n |-> 0 = @ (@ (n |-> 0)) ;
then reconsider N = n |-> 0 as Element of (Euclid n) by A17, TOPREAL3:45;
e is Element of (TOP-REAL k) by Lm1;
then A21: e0 in A by A1;
assume e in p ; :: thesis:
then e0 in B by A3, A21, A20;
then e0 in q by A14, XBOOLE_0:def 4;
then consider m being non zero Element of NAT such that
A22: OpenHypercube (e0,(1 / m)) c= q by A16, EUCLID_9:23;
set r = 1 / m;
take 1 / m ; :: thesis:
thus 1 / m > 0 by XREAL_1:139; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
N in OpenHypercube (N,(1 / m)) by EUCLID_9:11, XREAL_1:139;
then A23: N in product (Intervals (N,(1 / m))) by EUCLID_9:def 4;
assume A24: x in OpenHypercube (e,(1 / m)) ; :: thesis:
then reconsider w = x as Point of (TOP-REAL k) 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 A24, EUCLID_9:def 4;
then w ^ N in product (Intervals (e0,(1 / m))) by A23, A25, Th2;
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 A4, A14, A22, A26, XBOOLE_0:def 4;
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:

end;

then p is open by EUCLID_9:24;
then Ak in the topology of (TOP-REAL k) by A2, PRE_TOPC:def 2;
hence Ak is open by PRE_TOPC:def 2; :: thesis: