theorem :: FINTOPO5:13

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