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 = {} 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;