let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st n = 0 holds
for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
for p being Point of (TOP-REAL n) holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )
set TR = TOP-REAL n;
A1: Int ([#] (TOP-REAL n)) = [#] (TOP-REAL n) by TOPS_1:15;
let A, B be Subset of (TOP-REAL n); :: thesis: ( n = 0 implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
for p being Point of (TOP-REAL n) holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) ) )
assume A2: n = 0 ; :: thesis: for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds
for p being Point of (TOP-REAL n) holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )
A3: the carrier of (TOP-REAL n) = {(0. (TOP-REAL n))} by A2, EUCLID:77, EUCLID:22;
let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); :: thesis: ( h is being_homeomorphism implies for p being Point of (TOP-REAL n) holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) ) )
assume A4: h is being_homeomorphism ; :: thesis: for p being Point of (TOP-REAL n) holds
( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )
A5: dom h = [#] ((TOP-REAL n) | A) by A4, TOPS_2:def 5;
let p be Point of (TOP-REAL n); :: thesis: ( ( p in Fr A implies h . p in Fr B ) & ( p in Int A implies h . p in Int B ) )
[#] (TOP-REAL n) is open ;
hence ( p in Fr A implies h . p in Fr B ) by A3, ZFMISC_1:33; :: thesis: ( p in Int A implies h . p in Int B )
A6: A = [#] ((TOP-REAL n) | A) by PRE_TOPC:def 5;
A7: Int A c= A by TOPS_1:16;
assume p in Int A ; :: thesis: h . p in Int B
then A8: h . p in rng h by A7, A5, A6, FUNCT_1:def 3;
A9: B = [#] ((TOP-REAL n) | B) by PRE_TOPC:def 5;
then B = [#] (TOP-REAL n) by A8, ZFMISC_1:33, A3;
hence h . p in Int B by A8, A1, A9; :: thesis: verum