theorem :: FINTOPO5:16

for n being non zero Nat ex h being Function of (FTSS2 (n,1)),(FTSL1 n) st h is being_homeomorphism