let n, i be Element of NAT ; :: thesis: ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = Proj p,i
defpred S₁[ set , set ] means for p being Element of (TOP-REAL n) st $1 = p holds
$2 = Proj p,i;
A1: for x being set st x in REAL n holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

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

end;

ex f being Function of (REAL n),REAL st
for x being set 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 set st x in REAL n holds
for p being Element of (TOP-REAL n) st x = p holds
f . x = Proj p,i ;
the carrier of (TOP-REAL n) = REAL n by EUCLID:25;
then reconsider f1 = f as Function of (TOP-REAL n),R^1 by TOPMETR:24;
for p being Element of (TOP-REAL n) holds f1 . p = Proj p,i

proof

let p be Element of (TOP-REAL n); :: thesis: f1 . p = Proj p,i
p in the carrier of (TOP-REAL n) ;
then p in REAL n by EUCLID:25;
hence f1 . p = Proj 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 = Proj p,i ; :: thesis: verum