A1: now

let p be set ; :: thesis: ( p in REAL implies (reproj i,x) . p in REAL n )
assume p in REAL ; :: thesis: (reproj i,x) . p in REAL n
then reconsider r = p as Element of REAL ;
A2: (reproj i,x) . r = Replace x,i,r by Def5;
then reconsider IT = (reproj i,x) . r as FinSequence of REAL ;
len IT = len x by A2, FINSEQ_7:7
.= n by FINSEQ_1:def 18 ;
then reconsider IT = IT as Element of n -tuples_on REAL by FINSEQ_2:110;
IT is Element of REAL n ;
hence (reproj i,x) . p in REAL n ; :: thesis: verum

end;

dom (reproj i,x) = REAL by Def5;
hence reproj i,x is Function of REAL ,(REAL n) by A1, FUNCT_2:5; :: thesis: verum