let S, T be TopStruct ; :: thesis: for f being Function of S,T st f is being_homeomorphism holds

f " is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies f " is being_homeomorphism )

assume A1: f is being_homeomorphism ; :: thesis: f " is being_homeomorphism

then A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) by TOPS_2:def 5;

f " is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is being_homeomorphism implies f " is being_homeomorphism )

assume A1: f is being_homeomorphism ; :: thesis: f " is being_homeomorphism

then A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) by TOPS_2:def 5;

per cases
( ( not S is empty & not T is empty ) or S is empty or T is empty )
;

end;

suppose A3:
( S is empty or T is empty )
; :: thesis: f " is being_homeomorphism

A4:
f = {}
reconsider g = f as one-to-one onto PartFunc of {},{} by A4, FUNCTOR0:1;

A5: f " = g " by A2;

A6: ( dom (f ") = [#] T & rng (f ") = [#] S ) by A2, A4;

reconsider g1 = f " as one-to-one onto PartFunc of {},{} by A5;

(f ") " = g1 " by A2, A4;

hence f " is being_homeomorphism by A4, A6, A2, TOPS_2:def 5; :: thesis: verum

end;A5: f " = g " by A2;

A6: ( dom (f ") = [#] T & rng (f ") = [#] S ) by A2, A4;

reconsider g1 = f " as one-to-one onto PartFunc of {},{} by A5;

(f ") " = g1 " by A2, A4;

hence f " is being_homeomorphism by A4, A6, A2, TOPS_2:def 5; :: thesis: verum