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;

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

suppose ( not S is empty & not T is empty ) ; :: thesis: f " is being_homeomorphism

hence f " is being_homeomorphism by A1, TOPS_2:56; :: thesis: verum

end;

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

A4: f = {}

proof

per cases ( S is empty or T is empty ) by A3;

suppose S is empty ; :: thesis: f = {}

hence f = {} ; :: thesis: verum

end;

suppose T is empty ; :: thesis: f = {}

hence f = {} ; :: thesis: verum

end;

end;

end;

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;

end;