let X be RealNormSpace; :: thesis: for x being Point of (product <*X*>) holds NrProduct x = ||.x.||
let x be Point of (product <*X*>); :: thesis: NrProduct x = ||.x.||
A1: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
consider x1 being Point of X such that
A3: x = <*x1*> by Th12;
rng <*||.x1.||*> c= REAL ;
then reconsider Nx = <*||.x1.||*> as FinSequence of REAL by FINSEQ_1:def 4;
A4: dom Nx = {1} by FINSEQ_1:2, FINSEQ_1:38;

A5: now :: thesis: for i being Element of dom <*X*> holds Nx . i = ||.(x . i).||

let i be Element of dom <*X*>; :: thesis: Nx . i = ||.(x . i).||
A6: i = 1 by A1, TARSKI:def 1;
hence Nx . i = ||.x1.||
.= ||.(x . i).|| by A3, A6 ;
:: thesis: verum

end;

Product Nx = ||.x1.|| ;
hence NrProduct x = ||.x.|| by A1, A3, A4, A5, Th12, LOPBAN10:def 9; :: thesis: verum