theorem :: PRVECT_2:14

for G being RealNormSpace-Sequence st ( for i being Element of dom G holds G . i is complete ) holds
product G is complete