for X being RealNormSpace-Sequence
for x being Point of (product X) ex d being FinSequence of REAL st
( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) )