theorem :: LOPBAN14:26

for X being RealNormSpace st X is complete holds
product <*X*> is complete