theorem :: EUCLID:65

for n being Nat
for x being Real
for p being Point of (TOP-REAL n)
for r being real-valued Function st p = r holds
x * p = x (#) r ;