theorem :: TOPREALC:36

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 Th35;