theorem :: PDIFF_8:9

for n being non zero Element of NAT
for x being Element of REAL n
for r being Real
for i being Element of NAT holds (proj (i,n)) . (r * x) = r * ((proj (i,n)) . x)