theorem Th35: :: LOPBAN14:34

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for z being Element of (product (X ^ <*Y*>))
for y being Point of Y st z = x ^ <*y*> holds
NrProduct z = ||.y.|| * (NrProduct x)