theorem Th37: :: NDIFF_5:37

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)