let i be Element of NAT ; :: thesis: 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
let n be Nat; :: thesis: ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i
defpred S₁[ object , object ] means for p being Element of (TOP-REAL n) st $1 = p holds
$2 = p /. i;
A1: for x being object st x in REAL n holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in REAL n implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in REAL n ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider px = x as Element of (TOP-REAL n) by EUCLID:22;
consider q being Real, g being FinSequence of REAL such that
A2: g = px and
q = g /. i by Lm1;
for p being Element of (TOP-REAL n) st x = p holds
g /. i = p /. i by A2;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

ex f being Function of (REAL n),REAL st
for x being object st x in REAL n holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
then consider f being Function of (REAL n),REAL such that
A3: for x being object st x in REAL n holds
for p being Element of (TOP-REAL n) st x = p holds
f . x = p /. i ;
the carrier of (TOP-REAL n) = REAL n by EUCLID:22;
then reconsider f1 = f as Function of (TOP-REAL n),R^1 by TOPMETR:17;
for p being Element of (TOP-REAL n) holds f1 . p = p /. i

proof

let p be Element of (TOP-REAL n); :: thesis: f1 . p = p /. i
p in the carrier of (TOP-REAL n) ;
then p in REAL n by EUCLID:22;
hence f1 . p = p /. i by A3; :: thesis: verum

end;

hence ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i ; :: thesis: verum