deffunc H_{1}( Point of (REAL-NS n)) -> set = <*((proj (i,n)) . $1)*>;

A1: for x being Point of (REAL-NS n) holds H_{1}(x) is Element of (REAL-NS 1)

for x being Point of (REAL-NS n) holds f . x = H_{1}(x)
from FUNCT_2:sch 9(A1); :: thesis: verum

A1: for x being Point of (REAL-NS n) holds H

proof

thus
ex f being Function of (REAL-NS n),(REAL-NS 1) st
let x be Point of (REAL-NS n); :: thesis: H_{1}(x) is Element of (REAL-NS 1)

(proj (i,n)) . x in REAL by XREAL_0:def 1;

then A2: H_{1}(x) is FinSequence of REAL
by FINSEQ_1:74;

len H_{1}(x) = 1
by FINSEQ_1:39;

then H_{1}(x) is Element of 1 -tuples_on REAL
by A2, FINSEQ_2:92;

then H_{1}(x) in REAL 1
;

hence H_{1}(x) is Element of (REAL-NS 1)
by REAL_NS1:def 4; :: thesis: verum

end;(proj (i,n)) . x in REAL by XREAL_0:def 1;

then A2: H

len H

then H

then H

hence H

for x being Point of (REAL-NS n) holds f . x = H