let G be RealNormSpace-Sequence; :: thesis: for p being Point of (product G) holds
( 0. (product G) = p iff for i being Element of dom G holds p . i = 0. (G . i) )
let p be Point of (product G); :: thesis: ( 0. (product G) = p iff for i being Element of dom G holds p . i = 0. (G . i) )
reconsider p0 = p as Element of product (carr G) by EXTh10;
A1: dom (carr G) = dom G by LemmaX;
A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;
hence ( 0. (product G) = p implies for i being Element of dom G holds p . i = 0. (G . i) ) by A1, PRVECT_1:def 14; :: thesis: ( ( for i being Element of dom G holds p . i = 0. (G . i) ) implies 0. (product G) = p )
assume A3: for i being Element of dom G holds p . i = 0. (G . i) ; :: thesis: 0. (product G) = p
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 LemmaX;
p0 . i0 = 0. (G . i) by A3;
hence p0 . i0 = 0. (G . i0) ; :: thesis: verum
end;
hence 0. (product G) = p by A2, PRVECT_1:def 14; :: thesis: verum