theorem Th38: :: ORDEQ_01:38

for n being non zero Element of NAT
for i being Nat
for y1 being Point of (REAL-NS n)
for r being Real holds (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1)