let G be RealNormSpace-Sequence; :: thesis: for p, q, r being Point of (product G) holds
( p + q = r iff for i being Element of dom G holds r . i = (p . i) + (q . i) )
let p, q, r be Point of (product G); :: thesis: ( p + q = r iff for i being Element of dom G holds r . i = (p . i) + (q . i) )
reconsider p0 = p, q0 = q, r0 = r as Element of product (carr G) by EXTh10;
A2: product G = NORMSTR(# (product (carr G)),(zeros G),[:(addop G):],[:(multop G):],(productnorm G) #) by PRVECT_2:6;

hereby :: thesis: ( ( for i being Element of dom G holds r . i = (p . i) + (q . i) ) implies p + q = r )

assume A3: p + q = r ; :: thesis: for i being Element of dom G holds r . i = (p . i) + (q . i)

hereby :: thesis: verum

let i be Element of dom G; :: thesis: r . i = (p . i) + (q . i)
reconsider i0 = i as Element of dom (carr G) by LemmaX;
(addop G) . i0 = the addF of (G . i0) by PRVECT_1:def 12;
hence r . i = (p . i) + (q . i) by A2, A3, PRVECT_1:def 8; :: thesis: verum

end;

end;

assume A4: for i being Element of dom G holds r . i = (p . i) + (q . i) ; :: thesis: p + q = r
reconsider pq = p + q as Element of product (carr G) by EXTh10;
A5: ex g being Function st
( pq = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
A6: ex g being Function st
( r0 = g & dom g = dom (carr G) & ( for i being object st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;

now :: thesis: for i0 being object st i0 in dom pq holds
pq . i0 = r0 . i0

let i0 be object ; :: thesis: ( i0 in dom pq implies pq . i0 = r0 . i0 )
assume A7: i0 in dom pq ; :: thesis: pq . i0 = r0 . i0
then reconsider i1 = i0 as Element of dom G by LemmaX, A5;
reconsider i = i0 as Element of dom (carr G) by A5, A7;
(addop G) . i = the addF of (G . i) by PRVECT_1:def 12;
then pq . i0 = (p0 . i1) + (q0 . i1) by A2, PRVECT_1:def 8;
hence pq . i0 = r0 . i0 by A4; :: thesis: verum

end;

hence p + q = r by A5, A6; :: thesis: verum