let X be RealNormSpace; :: thesis: ( X is complete implies product <*X*> is complete )
A1: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then reconsider i = 1 as Element of dom <*X*> by TARSKI:def 1;
assume A2: X is complete ; :: thesis: product <*X*> is complete

now :: thesis: for i being Element of dom <*X*> holds <*X*> . i is complete

let i be Element of dom <*X*>; :: thesis: <*X*> . i is complete
i = 1 by A1, TARSKI:def 1;
hence <*X*> . i is complete by A2; :: thesis: verum

end;

hence product <*X*> is complete by PRVECT_2:14; :: thesis: verum