let n be Nat; for p1, p2, p3 being Point of (TOP-REAL n) holds |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
let p1, p2, p3 be Point of (TOP-REAL n); |((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
reconsider f1 = p1, f2 = p2, f3 = p3 as FinSequence of REAL by EUCLID:24;
reconsider q1 = p1, q2 = p2 as Element of REAL n by EUCLID:22;
len f2 = n
by CARD_1:def 7;
then A1:
( len f1 = len f2 & len f2 = len f3 )
by CARD_1:def 7;
thus
|((p1 + p2),p3)| = |(p1,p3)| + |(p2,p3)|
by A1, RVSUM_1:120; verum