let X be RealNormSpace-Sequence; :: thesis:
let x be Point of (product X); :: thesis:
consider Nx being FinSequence of REAL such that
A1: ( dom Nx = dom X & ( for i being Element of dom X holds Nx . i = ||.(x . i).|| ) ) and
A2: NrProduct x = Product Nx by DefNrPro;
thus ( ex i being Element of dom X st x . i = 0. (X . i) iff NrProduct x = 0 ) :: thesis:

assume ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis:
then consider i being Element of dom X such that
A3: x . i = 0. (X . i) ;
Nx . i = ||.(0. (X . i)).|| by A1, A3
.= 0 ;
hence NrProduct x = 0 by A1, A2, RVSUM_1:103; :: thesis:

end;

assume NrProduct x = 0 ; :: thesis:
then consider k being Nat such that
A5: ( k in dom Nx & Nx . k = 0 ) by A2, RVSUM_1:103;
reconsider i = k as Element of dom X by A1, A5;
||.(x . i).|| = 0 by A1, A5;
then x . i = 0. (X . i) by NORMSP_0:def 5;
hence ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis:

end;

thus ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x ) :: thesis:

assume A7: for i being Element of dom X holds not x . i = 0. (X . i) ; :: thesis:
for k being Element of NAT st k in dom Nx holds
Nx . k > 0

let k be Element of NAT ; :: thesis:
assume k in dom Nx ; :: thesis:
then reconsider i = k as Element of dom X by A1;
A9: Nx . i = ||.(x . i).|| by A1;
x . i <> 0. (X . i) by A7;
then Nx . k <> 0 by A9, NORMSP_0:def 5;
hence Nx . k > 0 by A9; :: thesis:

end;

end;