theorem Th19: :: LOPBAN14:18

for X being RealNormSpace
for x being Point of (product <*X*>) holds NrProduct x = ||.x.||