A1: p +* x,r is FinSequence of REAL by Th19;
A2: len p = n by FINSEQ_1:def 18;
Seg (len (p +* x,r)) = dom (p +* x,r) by FINSEQ_1:def 3
.= dom p by FUNCT_7:32
.= Seg n by A2, FINSEQ_1:def 3 ;
then len (p +* x,r) = n by FINSEQ_1:8;
then p +* x,r is Element of REAL n by A1, FINSEQ_2:110;
hence p +* x,r is Point of (TOP-REAL n) by EUCLID:25; :: thesis: verum