let n be Nat; :: thesis: for A, B being Subset of () st A is closed & B is closed holds
for h being Function of (() | A),(() | B) st h is being_homeomorphism holds
( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

let A, B be Subset of (); :: thesis: ( A is closed & B is closed implies for h being Function of (() | A),(() | 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 (() | A),(() | B) st h is being_homeomorphism holds
( h .: (Int A) = Int B & h .: (Fr A) = Fr B )

set TR = TOP-REAL n;
A3: [#] (() | A) = A by PRE_TOPC:def 5;
A4: Int B c= B by TOPS_1:16;
A5: [#] (() | B) = B by PRE_TOPC:def 5;
let h be Function of (() | A),(() | 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 = [#] (() | A) by ;
A8: rng h = [#] (() | B) by ;
A9: (Fr A) \/ (Int A) = (A \ (Int A)) \/ (Int A) by
.= A \/ (Int A) by XBOOLE_1:39
.= A by ;
thus A10: h .: (Int A) = Int B :: thesis: h .: (Fr A) = Fr B
proof
thus h .: (Int A) c= Int B :: according to XBOOLE_0:def 10 :: thesis: Int B c= h .: (Int A)
proof
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;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Int B or y in 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 ;
reconsider x = x as Point of () by A7, A3, A12;
assume A14: not y in h .: (Int A) ; :: thesis: contradiction
not x in Int A by ;
then x in Fr A by ;
then h . x in Fr B by Th10, A1, A6;
hence contradiction by A11, A13, TOPS_1:39, XBOOLE_0:3; :: thesis: verum
end;
Fr A = A \ (Int A) by ;
then h .: (Fr A) = (h .: A) \ (h .: (Int A)) by
.= B \ (h .: (Int A)) by
.= Fr B by ;
hence h .: (Fr A) = Fr B ; :: thesis: verum