let T be TopStruct ; :: thesis: for f being Function of T,T st T is empty holds
f is being_homeomorphism
let f be Function of T,T; :: thesis: ( T is empty implies f is being_homeomorphism )
assume A1: T is empty ; :: thesis: f is being_homeomorphism
then f = {}
.= id T by A1 ;
hence f is being_homeomorphism ; :: thesis: verum