let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st A is closed & B is closed holds

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

let A, B be Subset of (TOP-REAL n); :: thesis: ( A is closed & B is closed implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )

assume that

A1: A is closed and

A2: B is closed ; :: thesis: for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

set TR = TOP-REAL n;

A3: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

A4: Int B c= B by TOPS_1:16;

A5: [#] ((TOP-REAL n) | B) = B by PRE_TOPC:def 5;

let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); :: thesis: ( h is being_homeomorphism implies ( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )

assume A6: h is being_homeomorphism ; :: thesis: ( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

A7: dom h = [#] ((TOP-REAL n) | A) by A6, TOPS_2:def 5;

A8: rng h = [#] ((TOP-REAL n) | B) by A6, TOPS_2:def 5;

A9: (Fr A) \/ (Int A) = (A \ (Int A)) \/ (Int A) by A1, TOPS_1:43

.= A \/ (Int A) by XBOOLE_1:39

.= A by TOPS_1:16, XBOOLE_1:12 ;

thus A10: h .: (Int A) = Int B :: thesis: h .: (Fr A) = Fr B

then h .: (Fr A) = (h .: A) \ (h .: (Int A)) by A6, FUNCT_1:64

.= B \ (h .: (Int A)) by RELAT_1:113, A7, A8, A3, A5

.= Fr B by A10, A2, TOPS_1:43 ;

hence h .: (Fr A) = Fr B ; :: thesis: verum

for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

let A, B be Subset of (TOP-REAL n); :: thesis: ( A is closed & B is closed implies for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )

assume that

A1: A is closed and

A2: B is closed ; :: thesis: for h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st h is being_homeomorphism holds

( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

set TR = TOP-REAL n;

A3: [#] ((TOP-REAL n) | A) = A by PRE_TOPC:def 5;

A4: Int B c= B by TOPS_1:16;

A5: [#] ((TOP-REAL n) | B) = B by PRE_TOPC:def 5;

let h be Function of ((TOP-REAL n) | A),((TOP-REAL n) | B); :: thesis: ( h is being_homeomorphism implies ( h .: (Int A) = Int B & h .: (Fr A) = Fr B ) )

assume A6: h is being_homeomorphism ; :: thesis: ( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

A7: dom h = [#] ((TOP-REAL n) | A) by A6, TOPS_2:def 5;

A8: rng h = [#] ((TOP-REAL n) | B) by A6, TOPS_2:def 5;

A9: (Fr A) \/ (Int A) = (A \ (Int A)) \/ (Int A) by A1, TOPS_1:43

.= A \/ (Int A) by XBOOLE_1:39

.= A by TOPS_1:16, XBOOLE_1:12 ;

thus A10: h .: (Int A) = Int B :: thesis: h .: (Fr A) = Fr B

proof

Fr A = A \ (Int A)
by A1, TOPS_1:43;
thus
h .: (Int A) c= Int B
:: according to XBOOLE_0:def 10 :: thesis: Int B c= h .: (Int A)

assume A11: y in Int B ; :: thesis: y in h .: (Int A)

then consider x being object such that

A12: x in dom h and

A13: h . x = y by A4, A8, A5, FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A7, A3, A12;

assume A14: not y in h .: (Int A) ; :: thesis: contradiction

not x in Int A by A12, FUNCT_1:def 6, A14, A13;

then x in Fr A by A12, A9, A3, XBOOLE_0:def 3;

then h . x in Fr B by Th10, A1, A6;

hence contradiction by A11, A13, TOPS_1:39, XBOOLE_0:3; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Int B or y in h .: (Int A) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in h .: (Int A) or y in Int B )

assume y in h .: (Int A) ; :: thesis: y in Int B

then ex x being object st

( x in dom h & x in Int A & h . x = y ) by FUNCT_1:def 6;

hence y in Int B by A2, A6, Th11; :: thesis: verum

end;assume y in h .: (Int A) ; :: thesis: y in Int B

then ex x being object st

( x in dom h & x in Int A & h . x = y ) by FUNCT_1:def 6;

hence y in Int B by A2, A6, Th11; :: thesis: verum

assume A11: y in Int B ; :: thesis: y in h .: (Int A)

then consider x being object such that

A12: x in dom h and

A13: h . x = y by A4, A8, A5, FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL n) by A7, A3, A12;

assume A14: not y in h .: (Int A) ; :: thesis: contradiction

not x in Int A by A12, FUNCT_1:def 6, A14, A13;

then x in Fr A by A12, A9, A3, XBOOLE_0:def 3;

then h . x in Fr B by Th10, A1, A6;

hence contradiction by A11, A13, TOPS_1:39, XBOOLE_0:3; :: thesis: verum

then h .: (Fr A) = (h .: A) \ (h .: (Int A)) by A6, FUNCT_1:64

.= B \ (h .: (Int A)) by RELAT_1:113, A7, A8, A3, A5

.= Fr B by A10, A2, TOPS_1:43 ;

hence h .: (Fr A) = Fr B ; :: thesis: verum