theorem Th54: :: EUCLID_2:56

for n being Nat
for a being Real
for p, q being Point of (TOP-REAL n) st p,q are_orthogonal holds
a * p,q are_orthogonal