let n be Element of NAT ; :: thesis: for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i)
let p1, p2 be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i)
let i be Element of NAT ; :: thesis: ( i in Seg n implies Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i) )
assume A1: i in Seg n ; :: thesis: Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i)
reconsider w1 = p1 as Element of REAL n by EUCLID:25;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w5 = p2 as Element of REAL n by EUCLID:25;
reconsider w7 = w5 as Element of n -tuples_on REAL ;
reconsider w = p1 - p2 as Element of REAL n by EUCLID:25;
len w1 = n by FINSEQ_1:def 18;
then A2: i in dom w1 by A1, FINSEQ_1:def 3;
i in Seg (len w5) by A1, FINSEQ_1:def 18;
then A3: i in dom w5 by FINSEQ_1:def 3;
A4: Proj p1,i = w1 /. i by Def1
.= w3 . i by A2, PARTFUN1:def 8 ;
A5: Proj p2,i = w5 /. i by Def1
.= w7 . i by A3, PARTFUN1:def 8 ;
len w = n by FINSEQ_1:def 18;
then A6: i in dom w by A1, FINSEQ_1:def 3;
Proj (p1 - p2),i = w /. i by Def1
.= w . i by A6, PARTFUN1:def 8
.= (w3 - w7) . i by A4, A5, EUCLID:73
.= (w3 . i) - (w7 . i) by A4, A5, RVSUM_1:48
.= (Proj p1,i) - (Proj p2,i) by A4, A5, EUCLID:68 ;
hence Proj (p1 - p2),i = (Proj p1,i) - (Proj p2,i) ; :: thesis: verum