product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
then reconsider s = x as Element of product (carr X) ;
defpred S₁[ object , object ] means ex i being Element of dom X st
( $1 = i & $2 = ||.(x . i).|| );
A7: for n being Nat st n in Seg (len X) holds
ex d being Element of REAL st S₁[n,d]

let n be Nat; :: thesis:
assume n in Seg (len X) ; :: thesis:
then reconsider i = n as Element of dom X by FINSEQ_1:def 3;
reconsider d = ||.(x . i).|| as Element of REAL ;
take d ; :: thesis:
thus S₁[n,d] ; :: thesis:

end;

consider F being FinSequence of REAL such that
A8: ( len F = len X & ( for n being Nat st n in Seg (len X) holds
S₁[n,F /. n] ) ) from FINSEQ_4:sch 1(A7);
A9: dom F = dom X by A8, FINSEQ_3:29;
A10: for i being Element of dom X holds F . i = ||.(x . i).||

let i be Element of dom X; :: thesis:
i in dom X ;
then A11: i in Seg (len X) by FINSEQ_1:def 3;
reconsider n = i as Nat ;
consider j being Element of dom X such that
A12: ( n = j & F /. n = ||.(x . j).|| ) by A8, A11;
thus F . i = ||.(x . i).|| by A9, A12, PARTFUN1:def 6; :: thesis:

end;

set R = Product F;
0 <= Product F

end;

let k be Element of NAT ; :: thesis:
assume A17: k in dom F ; :: thesis:
then A18: F . k <> 0 by A15;
reconsider i = k as Element of dom X by A8, FINSEQ_3:29, A17;
F . i = ||.(x . i).|| by A10;
hence F . k > 0 by A18; :: thesis:

end;

end;

then reconsider R = Product F as non negative Real ;
take R ; :: thesis:
thus ex Nx being FinSequence of REAL st
( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) & R = Product Nx ) by A9, A10; :: thesis: