theorem Th11: :: NDIFF_5:11

for G being RealNormSpace-Sequence
for i being Element of dom G
for r being set
for x being Function st r in the carrier of (G . i) & x in product (carr G) holds
x +* (i,r) in the carrier of (product G)