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_2:def 7;

hence z . i = 0. (X . i) by A1, A2; :: thesis: verum

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_2:def 7;

hence z . i = 0. (X . i) by A1, A2; :: thesis: verum