let X be RealNormSpace-Sequence; :: thesis: for z being Element of (product X) st z = 0. (product X) holds
for i being Element of dom X holds z . i = 0. (X . i)
let z be Element of (product X); :: thesis: ( z = 0. (product X) implies for i being Element of dom X holds z . i = 0. (X . i) )
assume A1: z = 0. (product X) ; :: thesis: for i being Element of dom X holds z . i = 0. (X . i)
let i be Element of dom X; :: thesis: z . i = 0. (X . i)
A2: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;
reconsider j = i as Element of dom (carr X) by DCARXX;
(zeros X) . j = 0. (X . j) by PRVECT_1:def 14;
hence z . i = 0. (X . i) by A1, A2; :: thesis: verum