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