let X be RealNormSpace-Sequence; :: thesis: for x being Point of (product X) st ( for i being Element of dom X holds ||.(x . i).|| <= 1 ) holds
( 0 <= NrProduct x & NrProduct x <= 1 )
let x be Point of (product X); :: thesis: ( ( for i being Element of dom X holds ||.(x . i).|| <= 1 ) implies ( 0 <= NrProduct x & NrProduct x <= 1 ) )
assume A1: for i being Element of dom X holds ||.(x . i).|| <= 1 ; :: thesis: ( 0 <= NrProduct x & NrProduct x <= 1 )
consider F being FinSequence of REAL such that
A2: ( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(x . i).|| ) & NrProduct x = Product F ) by DefNrPro;
for i being Element of dom F holds
( 0 <= F . i & F . i <= 1 )

proof

let i be Element of dom F; :: thesis: ( 0 <= F . i & F . i <= 1 )
reconsider j = i as Element of dom X by A2;
A3: F . j = ||.(x . j).|| by A2;
thus 0 <= F . i by A3; :: thesis: F . i <= 1
thus F . i <= 1 by A1, A3; :: thesis: verum

end;

hence ( 0 <= NrProduct x & NrProduct x <= 1 ) by A2, LM281; :: thesis: verum