theorem Th29: :: EUCLID:57

for x being Real
for p being Point of (TOP-REAL 2) holds x * p = |[(x * (p `1)),(x * (p `2))]|