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