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

proof

let x be Point of ; :: thesis: H₁(x) is Element of
len H₁(x) = 1 by FINSEQ_1:56;
then H₁(x) is Element of 1 -tuples_on REAL by FINSEQ_2:110;
then H₁(x) in REAL 1 ;
hence H₁(x) is Element of 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 holds f . x = H₁(x) from FUNCT_2:sch 9(A1); :: thesis: verum