let G be RealNormSpace-Sequence; 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); ( 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 ( ( for i being Element of dom G holds r . i = (p . i) + (q . i) ) implies p + q = r )
end;
assume A4:
for i being Element of dom G holds r . i = (p . i) + (q . i)
; 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;
hence
p + q = r
by A5, A6; verum