for n being Element of NAT
for g being Function of I[01],(TOP-REAL n) holds g is Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67;