theorem Th34: :: NDIFF_5:34

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