theorem Th10: :: NDIFF_5:10

for G being RealNormSpace-Sequence holds the carrier of (product G) = product (carr G)