theorem :: EUCLID_2:20

for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for x being Real holds |(p1,(x * p2))| = x * |(p1,p2)| by Th17;