theorem :: PDIFF_8:12

for n being non zero Element of NAT
for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x - y) = ((proj (i,n)) . x) - ((proj (i,n)) . y)