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 AS0: ( 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 LM001;
X0: 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 AS1: 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)
X1: r0 . i = (p0 . i) + (qq0 . i) by ADD1, AS1, AS0, X0;
- 1 is Real by XREAL_0:def 1;
then qq0 . i = (- 1) * (q0 . i) by AS0, MLT1;
hence r0 . i = (p0 . i) - (q0 . i) by X1, RLVECT_1:16; :: thesis: verum

end;

end;

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

now

let i be Element of dom G; :: thesis: r0 . i = (p0 . i) + (qq0 . i)
- 1 is Real by XREAL_0:def 1;
then X2: qq0 . i = (- 1) * (q0 . i) by AS0, MLT1;
r0 . i = (p0 . i) - (q0 . i) by AS2;
hence r0 . i = (p0 . i) + (qq0 . i) by X2, RLVECT_1:16; :: thesis: verum

end;

hence p - q = r0 by X0, ADD1, AS0; :: thesis: verum