let X be RealNormSpace-Sequence; :: thesis:
let x be Point of (product X); :: thesis:
assume A1: for i being Element of dom X holds ||.(x . i).|| <= 1 ; :: thesis:
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 )

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

end;