for i being Element of NAT
for n being Nat ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i