theorem Th3: :: REAL_NS1:3

for n being Nat
for x being VECTOR of (REAL-NS n)
for y being Element of REAL n
for a being Real st x = y holds
a * x = a * y