theorem Th21: :: NDIFF_5:21

for G being RealNormSpace-Sequence
for i being Element of dom G
for xi being Element of (G . i) holds ||.((reproj (i,(0. (product G)))) . xi).|| = ||.xi.||