theorem :: NDIFF_5:43

for G being RealNormSpace-Sequence
for x, y being Element of product (carr G)
for Z being set holds x +* (y | Z) is Element of product (carr G) by CARD_3:79;