A1: p (#) r is FinSequence of REAL by RVSUM_1:145;
A2: len p = n by CARD_1:def 7;
Seg (len (p (#) r)) = dom (p (#) r) by FINSEQ_1:def 3
.= dom p by VALUED_1:def 5
.= Seg n by A2, FINSEQ_1:def 3 ;
then len (p (#) r) = n by FINSEQ_1:6;
then p (#) r is Element of REAL n by A1, FINSEQ_2:92;
hence r (#) p is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum