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