theorem :: NDIFF_5:36

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)