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

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