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

suppose not T is empty ; :: thesis: f /" is being_homeomorphism

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

end;

suppose T is empty ; :: thesis: f /" is being_homeomorphism

then A1: the carrier of T is empty ;
f /" = f " by TOPS_2:def 4
.= id T by A1 ;
hence f /" is being_homeomorphism by Th19; :: thesis: verum

end;

end;