A1: now :: thesis: for p being object st p in REAL holds
(reproj (i,x)) . p in REAL n

let p be object ; :: 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:5
.= n by CARD_1:def 7 ;
then reconsider IT = IT as Element of n -tuples_on REAL by FINSEQ_2:92;
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:3; :: thesis: verum