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 A1: ( 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 A2: dom (carr G) = Seg (len G) by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3 ;
A3: 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 A4: 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 A2;
(addop G) . i0 = the addF of (G . i0) by PRVECT_2:def 5;
hence r0 . i = (p0 . i) + (q0 . i) by A1, A4, A3, PRVECT_1:def 8; :: thesis: verum

end;

end;

assume A5: 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 Th10;
A6: 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;
A7: 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 :: thesis: for i0 being set st i0 in dom pq holds
pq . i0 = r0 . i0

let i0 be set ; :: thesis: ( i0 in dom pq implies pq . i0 = r0 . i0 )
assume A8: i0 in dom pq ; :: thesis: pq . i0 = r0 . i0
then reconsider i1 = i0 as Element of dom G by A2, A6;
reconsider i = i0 as Element of dom (carr G) by A8, A6;
(addop G) . i = the addF of (G . i) by PRVECT_2:def 5;
then pq . i0 = (p0 . i1) + (q0 . i1) by A1, A3, PRVECT_1:def 8;
hence pq . i0 = r0 . i0 by A5; :: thesis: verum

end;

hence p + q = r0 by A6, A7, FUNCT_1:2; :: thesis: verum