defpred S₁[ Element of (REAL-NS 1), Point of (REAL-NS n)] means ex q being Element of REAL ex z being Element of REAL n st
( $1 = <*q*> & z = x & $2 = (reproj (i,z)) . q );
A1: for r being Element of (REAL-NS 1) ex y being Element of (REAL-NS n) st S₁[r,y]

proof

reconsider z = x as Element of REAL n by REAL_NS1:def 4;
let r be Element of (REAL-NS 1); :: thesis: ex y being Element of (REAL-NS n) st S₁[r,y]
r is Element of REAL 1 by REAL_NS1:def 4;
then consider q being Element of REAL such that
A2: r = <*q*> by FINSEQ_2:97;
(reproj (i,z)) . q is Element of (REAL-NS n) by REAL_NS1:def 4;
hence ex y being Element of (REAL-NS n) st S₁[r,y] by A2; :: thesis: verum

end;

thus ex f being Function of (REAL-NS 1),(REAL-NS n) st
for r being Element of (REAL-NS 1) holds S₁[r,f . r] from FUNCT_2:sch 3(A1); :: thesis: verum