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

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

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

proof

let i be Element of dom G; :: thesis: r . i = (p . i) - (q . i)
A4: r0 . i = (p0 . i) + (qq0 . i) by EXTh12, A3, A2;
qq0 . i = (- 1) * (q0 . i) by EXTh13;
hence r . i = (p . i) - (q . i) by A4, RLVECT_1:16; :: thesis: verum

end;

end;

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

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 EXTh13;
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 = r by A2, EXTh12; :: thesis: verum