A1:
p +* (x,r) is FinSequence of REAL
by RVSUM_1:145;

A2: len p = n by CARD_1:def 7;

Seg (len (p +* (x,r))) = dom (p +* (x,r)) by FINSEQ_1:def 3

.= dom p by FUNCT_7:30

.= Seg n by A2, FINSEQ_1:def 3 ;

then len (p +* (x,r)) = n by FINSEQ_1:6;

then p +* (x,r) is Element of REAL n by A1, FINSEQ_2:92;

hence p +* (x,r) is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum

A2: len p = n by CARD_1:def 7;

Seg (len (p +* (x,r))) = dom (p +* (x,r)) by FINSEQ_1:def 3

.= dom p by FUNCT_7:30

.= Seg n by A2, FINSEQ_1:def 3 ;

then len (p +* (x,r)) = n by FINSEQ_1:6;

then p +* (x,r) is Element of REAL n by A1, FINSEQ_2:92;

hence p +* (x,r) is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum