let i, j be Element of NAT ; :: thesis: ex f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st
( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) )
set TRi = TOP-REAL i;
set TRj = TOP-REAL j;
set TRij = TOP-REAL (i + j);
set tri = TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #);
set trj = TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #);
set trij = TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #);
A1: TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #) = TopSpaceMetr (Euclid j) by EUCLID:def 8;
( TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) = TopSpaceMetr (Euclid (i + j)) & TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #) = TopSpaceMetr (Euclid i) ) by EUCLID:def 8;
then consider f being Function of [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #):],TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) such that
A2: f is being_homeomorphism and
A3: for fi, fj being FinSequence st [fi,fj] in dom f holds
f . (fi,fj) = fi ^ fj by A1, TOPREAL7:26;
rng f = [#] TopStruct(# the carrier of (TOP-REAL (i + j)), the topology of (TOP-REAL (i + j)) #) by A2, TOPS_2:60;
then A4: rng f = [#] (TOP-REAL (i + j)) ;
A5: [#] [:(TOP-REAL i),(TOP-REAL j):] = [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by BORSUK_1:def 2;
A6: [:(TOP-REAL i),(TOP-REAL j):] = [:(TOP-REAL i),(TOP-REAL j):] | ([#] [:(TOP-REAL i),(TOP-REAL j):]) by TSEP_1:3
.= [:((TOP-REAL i) | ([#] (TOP-REAL i))),((TOP-REAL j) | ([#] (TOP-REAL j))):] by A5, BORSUK_3:22
.= [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),((TOP-REAL j) | ([#] (TOP-REAL j))):] by TSEP_1:93
.= [:TopStruct(# the carrier of (TOP-REAL i), the topology of (TOP-REAL i) #),TopStruct(# the carrier of (TOP-REAL j), the topology of (TOP-REAL j) #):] by TSEP_1:93 ;
then reconsider F = f as Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) ;
A7: now :: thesis: for P being Subset of [:(TOP-REAL i),(TOP-REAL j):] holds F .: (Cl P) = Cl (F .: P)
let P be Subset of [:(TOP-REAL i),(TOP-REAL j):]; :: thesis: F .: (Cl P) = Cl (F .: P)
thus F .: (Cl P) = Cl (f .: P) by A2, A6, TOPS_2:60
.= Cl (F .: P) by TOPS_3:80 ; :: thesis: verum
end;
take F ; :: thesis: ( F is being_homeomorphism & ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj ) )
A8: F is one-to-one by A2, TOPS_2:60;
dom F = [#] [:(TOP-REAL i),(TOP-REAL j):] by A2, A6, TOPS_2:60;
hence F is being_homeomorphism by A4, A7, A8, TOPS_2:60; :: thesis: for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj
let fi be Element of (TOP-REAL i); :: thesis: for fj being Element of (TOP-REAL j) holds F . (fi,fj) = fi ^ fj
let fj be Element of (TOP-REAL j); :: thesis: F . (fi,fj) = fi ^ fj
dom F = [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by A5, FUNCT_2:def 1;
then [fi,fj] in dom F by ZFMISC_1:87;
hence F . (fi,fj) = fi ^ fj by A3; :: thesis: verum