let G be RealNormSpace-Sequence; :: thesis: for p0 being Element of product (carr G) holds
( 0. (product G) = p0 iff for i being Element of dom G holds p0 . i = 0. (G . i) )
let p0 be Element of product (carr G); :: thesis: ( 0. (product G) = p0 iff for i being Element of dom G holds p0 . i = 0. (G . i) )
A1: dom (carr G) = dom G by Lm1;
A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
hence ( 0. (product G) = p0 implies for i being Element of dom G holds p0 . i = 0. (G . i) ) by A1, PRVECT_1:def 14; :: thesis: ( ( for i being Element of dom G holds p0 . i = 0. (G . i) ) implies 0. (product G) = p0 )
assume A3: for i being Element of dom G holds p0 . i = 0. (G . i) ; :: thesis: 0. (product G) = p0

now :: thesis: for i0 being Element of dom (carr G) holds p0 . i0 = 0. (G . i0)

let i0 be Element of dom (carr G); :: thesis: p0 . i0 = 0. (G . i0)
reconsider i = i0 as Element of dom G by Lm1;
p0 . i = 0. (G . i) by A3;
hence p0 . i0 = 0. (G . i0) ; :: thesis: verum

end;

hence 0. (product G) = p0 by A2, PRVECT_1:def 14; :: thesis: verum