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