let n, i be Element of NAT ; :: thesis: for y1, y2 being Point of (REAL-NS n) holds (Proj i,n) . (y1 + y2) = ((Proj i,n) . y1) + ((Proj i,n) . y2)
let y1, y2 be Point of (REAL-NS n); :: thesis: (Proj i,n) . (y1 + y2) = ((Proj i,n) . y1) + ((Proj i,n) . y2)
reconsider yy1 = y1, yy2 = y2 as Element of REAL n by REAL_NS1:def 4;
reconsider ry1 = yy1 . i as Element of REAL ;
reconsider ry2 = yy2 . i as Element of REAL ;
( (Proj i,n) . y1 = <*((proj i,n) . y1)*> & (Proj i,n) . y2 = <*((proj i,n) . y2)*> ) by PDIFF_1:def 4;
then Q1: ( (Proj i,n) . y1 = <*ry1*> & (Proj i,n) . y2 = <*ry2*> ) by PDIFF_1:def 1;
Q3: ( <*ry1*> is Element of REAL 1 & <*ry2*> is Element of REAL 1 ) by FINSEQ_2:118;
(Proj i,n) . (y1 + y2) = <*((proj i,n) . (y1 + y2))*> by PDIFF_1:def 4
.= <*((proj i,n) . (yy1 + yy2))*> by REAL_NS1:2
.= <*((yy1 + yy2) . i)*> by PDIFF_1:def 1
.= <*((yy1 . i) + (yy2 . i))*> by RVSUM_1:27
.= <*ry1*> + <*ry2*> by RVSUM_1:29 ;
hence (Proj i,n) . (y1 + y2) = ((Proj i,n) . y1) + ((Proj i,n) . y2) by Q1, Q3, REAL_NS1:2; :: thesis: verum