let G be RealNormSpace-Sequence; :: thesis: for p, q being Point of (product G)
for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds
( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )
let p, q be Point of (product G); :: thesis: for r0, p0, q0 being Element of product (carr G) st p = p0 & q = q0 holds
( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )
let r0, p0, q0 be Element of product (carr G); :: thesis: ( p = p0 & q = q0 implies ( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) ) )
assume AS0: ( p = p0 & q = q0 ) ; :: thesis: ( p + q = r0 iff for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) )
len (carr G) = len G by PRVECT_2:def 4;
then B1: dom (carr G) = Seg (len G) by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
P1: 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 r0 . i = (p0 . i) + (q0 . i) ) implies p + q = r0 )

assume AS1: p + q = r0 ; :: thesis: for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i)

hereby :: thesis: verum

let i be Element of dom G; :: thesis: r0 . i = (p0 . i) + (q0 . i)
reconsider i0 = i as Element of dom (carr G) by B1;
(addop G) . i0 = the addF of (G . i0) by PRVECT_2:def 5;
hence r0 . i = (p0 . i) + (q0 . i) by AS0, AS1, P1, PRVECT_1:def 8; :: thesis: verum

end;

end;

assume AS: for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) ; :: thesis: p + q = r0
reconsider pq = p + q as Element of product (carr G) by LM001;
X1: ex g being Function st
( pq = g & dom g = dom (carr G) & ( for i being set st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;
X2: ex g being Function st
( r0 = g & dom g = dom (carr G) & ( for i being set st i in dom (carr G) holds
g . i in (carr G) . i ) ) by CARD_3:def 5;

now

let i0 be set ; :: thesis: ( i0 in dom pq implies pq . i0 = r0 . i0 )
assume AS1: i0 in dom pq ; :: thesis: pq . i0 = r0 . i0
then reconsider i1 = i0 as Element of dom G by B1, X1;
reconsider i = i0 as Element of dom (carr G) by AS1, X1;
(addop G) . i = the addF of (G . i) by PRVECT_2:def 5;
then pq . i0 = (p0 . i1) + (q0 . i1) by AS0, P1, PRVECT_1:def 8;
hence pq . i0 = r0 . i0 by AS; :: thesis: verum

end;

hence p + q = r0 by X1, X2, FUNCT_1:2; :: thesis: verum