defpred S_{1}[ 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_{1}[r,y]

for r being Element of (REAL-NS 1) holds S_{1}[r,f . r]
from FUNCT_2:sch 3(A1); :: thesis: verum

( $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

proof

thus
ex f being Function of (REAL-NS 1),(REAL-NS n) st
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_{1}[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_{1}[r,y]
by A2; :: thesis: verum

end;let r be Element of (REAL-NS 1); :: thesis: ex y being Element of (REAL-NS n) st S

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

for r being Element of (REAL-NS 1) holds S