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]

proof

let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being Element of REAL st S₁[n,d] )
assume n in Seg (len X) ; :: thesis: ex d being Element of REAL st S₁[n,d]
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: S₁[n,d]
thus S₁[n,d] ; :: thesis: verum

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).||

proof

let i be Element of dom X; :: thesis: F . i = ||.(x . i).||
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: verum

end;

set R = Product F;
0 <= Product F

proof

per cases ( ex i being Nat st
( i in dom F & F . i = 0 ) or for i being Nat holds
( not i in dom F or not F . i = 0 ) ) ;

suppose ex i being Nat st
( i in dom F & F . i = 0 ) ; :: thesis: 0 <= Product F

hence 0 <= Product F by RVSUM_1:103; :: thesis: verum

end;

suppose A15: for i being Nat holds
( not i in dom F or not F . i = 0 ) ; :: thesis: 0 <= Product F

for k being Element of NAT st k in dom F holds
F . k > 0

proof

let k be Element of NAT ; :: thesis: ( k in dom F implies F . k > 0 )
assume A17: k in dom F ; :: thesis: F . k > 0
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: verum

end;

hence 0 <= Product F by NAT_4:42; :: thesis: verum

end;

end;

end;

then reconsider R = Product F as non negative Real ;
take R ; :: thesis: 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 )
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: verum