theorem :: TOPREALC:38

for X being set
for n being Nat
for r being Real
for f being Function of X,(TOP-REAL n) holds f [/] r is Function of X,(TOP-REAL n) by Th37;