for X being RealNormSpace-Sequence
for x being Point of (product X) st ( for i being Element of dom X holds ||.(x . i).|| <= 1 ) holds
( 0 <= NrProduct x & NrProduct x <= 1 )