for X being set
for n being Nat
for f being Function of X,(TOP-REAL n) holds <-> f is Function of X,(TOP-REAL n)