theorem Th35: :: NDIFF_5:35

for G being RealNormSpace-Sequence
for i being Element of dom G
for x, y being Point of (product G) holds (proj i) . (x + y) = ((proj i) . x) + ((proj i) . y)