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) )
reconsider qq0 = (- 1) * q as Element of product (carr G) by Th10;
A2: p - q = p + ((- 1) * q) by RLVECT_1:16;

hereby :: thesis: ( ( for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i) ) implies p - q = r0 )

assume A3: p - q = r0 ; :: thesis: for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i)
thus for i being Element of dom G holds r0 . i = (p0 . i) - (q0 . i) :: thesis: verum

proof

let i be Element of dom G; :: thesis: r0 . i = (p0 . i) - (q0 . i)
A4: r0 . i = (p0 . i) + (qq0 . i) by Th12, A3, A1, A2;
qq0 . i = (- 1) * (q0 . i) by A1, Th13;
hence r0 . i = (p0 . i) - (q0 . i) by A4, RLVECT_1:16; :: thesis: verum

end;

end;

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

now :: thesis: for i being Element of dom G holds r0 . i = (p0 . i) + (qq0 . i)

let i be Element of dom G; :: thesis: r0 . i = (p0 . i) + (qq0 . i)
A6: qq0 . i = (- 1) * (q0 . i) by A1, Th13;
r0 . i = (p0 . i) - (q0 . i) by A5;
hence r0 . i = (p0 . i) + (qq0 . i) by A6, RLVECT_1:16; :: thesis: verum

end;

hence p - q = r0 by A2, Th12, A1; :: thesis: verum