theorem :: PDIFF_8:10

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)