theorem Th34: :: LOPBAN14:33

for X being RealNormSpace-Sequence
for x being Element of (product X)
for Y being RealNormSpace
for y being Point of Y holds x ^ <*y*> is Point of (product (X ^ <*Y*>))