let n be Element of NAT ; for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
let p1, p2 be Point of (TOP-REAL n); for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
let i be Element of NAT ; ( i in Seg n implies (p1 - p2) /. i = (p1 /. i) - (p2 /. i) )
reconsider w1 = p1 as Element of REAL n by EUCLID:22;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w5 = p2 as Element of REAL n by EUCLID:22;
reconsider w7 = w5 as Element of n -tuples_on REAL ;
reconsider w = p1 - p2 as Element of REAL n by EUCLID:22;
assume A1:
i in Seg n
; (p1 - p2) /. i = (p1 /. i) - (p2 /. i)
then
i in Seg (len w5)
by CARD_1:def 7;
then A2:
i in dom w5
by FINSEQ_1:def 3;
len w1 = n
by CARD_1:def 7;
then
i in dom w1
by A1, FINSEQ_1:def 3;
then A3:
p1 /. i = w3 . i
by PARTFUN1:def 6;
len w = n
by CARD_1:def 7;
then A4:
i in dom w
by A1, FINSEQ_1:def 3;
A5:
p2 /. i = w7 . i
by A2, PARTFUN1:def 6;
(p1 - p2) /. i =
w . i
by A4, PARTFUN1:def 6
.=
(w3 - w7) . i
.=
(p1 /. i) - (p2 /. i)
by A3, A5, RVSUM_1:27
;
hence
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
; verum