for i, n being Nat
for f being Function of (TOP-REAL i),(TOP-REAL n) holds f (-) is Function of (TOP-REAL i),(TOP-REAL n)