let i, n be 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 by XREAL_0:def 1;
reconsider ry2 = yy2 . i as Element of REAL by XREAL_0:def 1;
( (Proj (i,n)) . y1 = <*((proj (i,n)) . y1)*> & (Proj (i,n)) . y2 = <*((proj (i,n)) . y2)*> ) by PDIFF_1:def 4;
then A1: ( (Proj (i,n)) . y1 = <*ry1*> & (Proj (i,n)) . y2 = <*ry2*> ) by PDIFF_1:def 1;
A2: ( <*ry1*> is Element of REAL 1 & <*ry2*> is Element of REAL 1 ) by FINSEQ_2:98;
(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:11
.= <*ry1*> + <*ry2*> by RVSUM_1:13 ;
hence (Proj (i,n)) . (y1 + y2) = ((Proj (i,n)) . y1) + ((Proj (i,n)) . y2) by A1, A2, REAL_NS1:2; :: thesis: verum