A1:
p1 /" p2 is FinSequence of REAL
by RVSUM_1:145;

A2: ( len p1 = n & len p2 = n ) by CARD_1:def 7;

Seg (len (p1 /" p2)) = dom (p1 /" p2) by FINSEQ_1:def 3

.= (dom p1) /\ (dom p2) by VALUED_1:16

.= (Seg n) /\ (dom p2) by A2, FINSEQ_1:def 3

.= (Seg n) /\ (Seg n) by A2, FINSEQ_1:def 3 ;

then len (p1 /" p2) = n by FINSEQ_1:6;

then p1 /" p2 is Element of REAL n by A1, FINSEQ_2:92;

hence p1 /" p2 is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum

A2: ( len p1 = n & len p2 = n ) by CARD_1:def 7;

Seg (len (p1 /" p2)) = dom (p1 /" p2) by FINSEQ_1:def 3

.= (dom p1) /\ (dom p2) by VALUED_1:16

.= (Seg n) /\ (dom p2) by A2, FINSEQ_1:def 3

.= (Seg n) /\ (Seg n) by A2, FINSEQ_1:def 3 ;

then len (p1 /" p2) = n by FINSEQ_1:6;

then p1 /" p2 is Element of REAL n by A1, FINSEQ_2:92;

hence p1 /" p2 is Point of (TOP-REAL n) by EUCLID:22; :: thesis: verum