let n, k be Nat; :: thesis: for An being Subset of ()
for Ak being Subset of () st k <= n & An = { v where v is Element of () : v | k in Ak } holds
( An is open iff Ak is open )

let An be Subset of (); :: thesis: for Ak being Subset of () st k <= n & An = { v where v is Element of () : v | k in Ak } holds
( An is open iff Ak is open )

let Ak be Subset of (); :: thesis: ( k <= n & An = { v where v is Element of () : v | k in Ak } implies ( An is open iff Ak is open ) )
assume k <= n ; :: thesis: ( not An = { v where v is Element of () : v | k in Ak } or ( An is open iff Ak is open ) )
then reconsider nk = n - k as Element of NAT by NAT_1:21;
A1: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider an = An as Subset of () ;
A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider ak = Ak as Subset of () ;
assume A3: An = { v where v is Element of () : v | k in Ak } ; :: thesis: ( An is open iff Ak is open )
hereby :: thesis: ( Ak is open implies An is open )
assume An is open ; :: thesis: Ak is open
then an in the topology of () by PRE_TOPC:def 2;
then A4: an is open by ;
for e being Point of () st e in ak holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= ak )
proof
( len (nk |-> 0) = nk & @ (@ (nk |-> 0)) = nk |-> 0 ) by CARD_1:def 7;
then reconsider nk0 = nk |-> 0 as Point of (Euclid nk) by TOPREAL3:45;
let e be Point of (); :: thesis: ( e in ak implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= ak ) )

A5: ( @ (@ (e ^ (nk |-> 0))) = e ^ (nk |-> 0) & len (e ^ nk0) = n ) by CARD_1:def 7;
then reconsider en = e ^ nk0 as Point of () by TOPREAL3:45;
reconsider En = e ^ nk0 as Point of () by ;
len e = k by CARD_1:def 7;
then dom e = Seg k by FINSEQ_1:def 3;
then A6: e = En | k by FINSEQ_1:21;
assume e in ak ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= ak )

then en in an by A3, A6;
then consider m being non zero Element of NAT such that
A7: OpenHypercube (en,(1 / m)) c= an by ;
take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= ak )
thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= ak
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in ak )
assume A8: y in OpenHypercube (e,r) ; :: thesis: y in ak
then reconsider p = y as Point of () ;
A9: p in product (Intervals (e,r)) by ;
reconsider P = p as Point of () by A2;
nk0 in OpenHypercube (nk0,r) by ;
then A10: nk0 in product (Intervals (nk0,r)) by EUCLID_9:def 4;
(Intervals (e,r)) ^ (Intervals (nk0,r)) = Intervals (en,r) by Th1;
then P ^ nk0 in product (Intervals (en,r)) by A10, A9, Th2;
then P ^ nk0 in OpenHypercube (en,r) by EUCLID_9:def 4;
then P ^ nk0 in an by A7;
then consider v being Element of () such that
A11: ( v = P ^ nk0 & v | k in Ak ) by A3;
len P = k by CARD_1:def 7;
then dom P = Seg k by FINSEQ_1:def 3;
hence y in ak by ; :: thesis: verum
end;
then ak is open by EUCLID_9:24;
then ak in the topology of () by ;
hence Ak is open by PRE_TOPC:def 2; :: thesis: verum
end;
assume Ak is open ; :: thesis: An is open
then ak in the topology of () by PRE_TOPC:def 2;
then A12: ak is open by ;
for e being Point of () st e in an holds
ex r being Real st
( r > 0 & OpenHypercube (e,r) c= an )
proof
let e be Point of (); :: thesis: ( e in an implies ex r being Real st
( r > 0 & OpenHypercube (e,r) c= an ) )

assume e in an ; :: thesis: ex r being Real st
( r > 0 & OpenHypercube (e,r) c= an )

then consider v being Element of () such that
A13: e = v and
A14: v | k in Ak by A3;
reconsider vk = v | k as Point of () by A14;
A15: len vk = k by CARD_1:def 7;
@ (@ vk) = vk ;
then reconsider Vk = vk as Point of () by ;
consider m being non zero Element of NAT such that
A16: OpenHypercube (Vk,(1 / m)) c= ak by ;
take r = 1 / m; :: thesis: ( r > 0 & OpenHypercube (e,r) c= an )
thus r > 0 by XREAL_1:139; :: thesis: OpenHypercube (e,r) c= an
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in OpenHypercube (e,r) or y in an )
assume A17: y in OpenHypercube (e,r) ; :: thesis: y in an
then A18: y in product (Intervals (e,r)) by EUCLID_9:def 4;
reconsider Y = y as Point of () by ;
A19: len v = n by CARD_1:def 7;
consider q being FinSequence such that
A20: @ (@ v) = vk ^ q by FINSEQ_1:80;
reconsider q = q as FinSequence of REAL by ;
len v = (len vk) + (len q) by ;
then reconsider Q = q as Point of (Euclid nk) by ;
(Intervals (Vk,r)) ^ (Intervals (Q,r)) = Intervals (e,r) by ;
then consider p1, p2 being FinSequence such that
A21: y = p1 ^ p2 and
A22: p1 in product (Intervals (Vk,r)) and
p2 in product (Intervals (Q,r)) by ;
A23: p1 in OpenHypercube (Vk,(1 / m)) by ;
then len p1 = k by ;
then Y | k = Y | (dom p1) by FINSEQ_1:def 3
.= p1 by ;
hence y in an by A3, A16, A23; :: thesis: verum
end;
then an is open by EUCLID_9:24;
then an in the topology of () by ;
hence An is open by PRE_TOPC:def 2; :: thesis: verum