let n be non zero Element of NAT ; :: thesis: for x, y being Point of (REAL-NS n)
for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
let x, y be Point of (REAL-NS n); :: thesis: for i being Nat holds (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
let i be Nat; :: thesis: (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y)
reconsider x1 = x, y1 = y as Element of REAL n by REAL_NS1:def 4;
reconsider rx = x1 . i, ry = y1 . i as Element of REAL by XREAL_0:def 1;
( (Proj (i,n)) . x = <*((proj (i,n)) . x)*> & (Proj (i,n)) . y = <*((proj (i,n)) . y)*> ) by PDIFF_1:def 4;
then A1: ( (Proj (i,n)) . x = <*rx*> & (Proj (i,n)) . y = <*ry*> ) by PDIFF_1:def 1;
A2: ( <*rx*> is Element of REAL 1 & <*ry*> is Element of REAL 1 ) by FINSEQ_2:98;
(Proj (i,n)) . (x - y) = <*((proj (i,n)) . (x - y))*> by PDIFF_1:def 4
.= <*((proj (i,n)) . (x1 - y1))*> by REAL_NS1:5
.= <*((x1 - y1) . i)*> by PDIFF_1:def 1
.= <*((x1 . i) - (y1 . i))*> by RVSUM_1:27
.= <*rx*> - <*ry*> by RVSUM_1:29 ;
hence (Proj (i,n)) . (x - y) = ((Proj (i,n)) . x) - ((Proj (i,n)) . y) by A1, A2, REAL_NS1:5; :: thesis: verum