deffunc H₁( Point of (REAL-NS n)) -> set = <*((proj (i,n)) . $1)*>;
A1: for x being Point of (REAL-NS n) holds H₁(x) is Element of (REAL-NS 1)

proof

let x be Point of (REAL-NS n); :: thesis: H₁(x) is Element of (REAL-NS 1)
(proj (i,n)) . x in REAL by XREAL_0:def 1;
then A2: H₁(x) is FinSequence of REAL by FINSEQ_1:74;
len H₁(x) = 1 by FINSEQ_1:39;
then H₁(x) is Element of 1 -tuples_on REAL by A2, FINSEQ_2:92;
then H₁(x) in REAL 1 ;
hence H₁(x) is Element of (REAL-NS 1) by REAL_NS1:def 4; :: thesis: verum

end;

thus ex f being Function of (REAL-NS n),(REAL-NS 1) st
for x being Point of (REAL-NS n) holds f . x = H₁(x) from FUNCT_2:sch 9(A1); :: thesis: verum