for f being Function of REAL,REAL holds f is Function of R^1,(R^1 | (R^1 (rng f)))