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