let X be RealNormSpace-Sequence; :: thesis: for x being Point of (product X) holds
( ( ex i being Element of dom X st x . i = 0. (X . i) implies NrProduct x = 0 ) & ( NrProduct x = 0 implies ex i being Element of dom X st x . i = 0. (X . i) ) & ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x ) )
let x be Point of (product X); :: thesis: ( ( ex i being Element of dom X st x . i = 0. (X . i) implies NrProduct x = 0 ) & ( NrProduct x = 0 implies ex i being Element of dom X st x . i = 0. (X . i) ) & ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x ) )
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: ( ( for i being Element of dom X holds not x . i = 0. (X . i) ) implies 0 < NrProduct x )

proof

hereby :: thesis: ( NrProduct x = 0 implies ex i being Element of dom X st x . i = 0. (X . i) )

assume ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis: NrProduct x = 0
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: verum

end;

assume NrProduct x = 0 ; :: thesis: ex i being Element of dom X st x . i = 0. (X . i)
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: verum

end;

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

proof

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

proof

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

end;

hence 0 < NrProduct x by A2, NAT_4:42; :: thesis: verum

end;