theorem Th17: :: EUCLID_2:19

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