A1: now :: thesis: for p being object st p in REAL holds

(reproj (i,x)) . p in REAL n

dom (reproj (i,x)) = REAL
by Def5;(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;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

hence reproj (i,x) is Function of REAL,(REAL n) by A1, FUNCT_2:3; :: thesis: verum