theorem Th18: :: LOPBAN14:17

for X being RealNormSpace
for s being Point of (product <*X*>)
for i being Element of dom <*X*> holds reproj (i,s) = IsoCPNrSP X