theorem Th27: :: PDIFF_6:27

for i, n 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)