let G be RealNormSpace-Sequence; :: thesis: for x being VECTOR of (product G)

for y being Element of product (carr G) st x = y holds

||.x.|| = |.(normsequence (G,y)).|

let x be VECTOR of (product G); :: thesis: for y being Element of product (carr G) st x = y holds

||.x.|| = |.(normsequence (G,y)).|

let y be Element of product (carr G); :: thesis: ( x = y implies ||.x.|| = |.(normsequence (G,y)).| )

assume A1: x = y ; :: thesis: ||.x.|| = |.(normsequence (G,y)).|

product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

hence ||.x.|| = |.(normsequence (G,y)).| by A1, Def12; :: thesis: verum

for y being Element of product (carr G) st x = y holds

||.x.|| = |.(normsequence (G,y)).|

let x be VECTOR of (product G); :: thesis: for y being Element of product (carr G) st x = y holds

||.x.|| = |.(normsequence (G,y)).|

let y be Element of product (carr G); :: thesis: ( x = y implies ||.x.|| = |.(normsequence (G,y)).| )

assume A1: x = y ; :: thesis: ||.x.|| = |.(normsequence (G,y)).|

product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by Th6;

hence ||.x.|| = |.(normsequence (G,y)).| by A1, Def12; :: thesis: verum