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;

hence p (/) r is Element of REAL n by A1, FINSEQ_2:92; :: thesis: verum

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;

hence p (/) r is Element of REAL n by A1, FINSEQ_2:92; :: thesis: verum