theorem :: RVSUM_1:141

for n being Nat
for a being Real
for p, q being Element of n -tuples_on REAL st p,q are_orthogonal holds
a * p,q are_orthogonal