let G be RealNormSpace-Sequence; 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); 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); ( 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 )
; ( 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_1:def 11;
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 ( ( for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i) ) implies p + q = r0 )
assume A4:
p + q = r0
;
for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i)
end;
assume A5:
for i being Element of dom G holds r0 . i = (p0 . i) + (q0 . i)
; 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 object 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 object st i in dom (carr G) holds
g . i in (carr G) . i ) )
by CARD_3:def 5;
hence
p + q = r0
by A6, A7, FUNCT_1:2; verum