let n be Element of NAT ; :: thesis: for g being Function of I[01] ,(TOP-REAL n) ex f being Function of (Closed-Interval-MSpace 0 ,1),(Euclid n) st f = g
let g be Function of I[01] ,(TOP-REAL n); :: thesis: ex f being Function of (Closed-Interval-MSpace 0 ,1),(Euclid n) st f = g
the carrier of (Euclid n) = the carrier of (TOP-REAL n) by TOPMETR:16;
hence ex f being Function of (Closed-Interval-MSpace 0 ,1),(Euclid n) st f = g by Lm3; :: thesis: verum