let n be non zero Element of NAT ; :: thesis: for i being Nat
for y1, y2 being Point of (REAL-NS n) holds (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2)
let i 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 Real ;
reconsider ry2 = yy2 . i as Real ;
A1: ( (proj (i,n)) . y1 = ry1 & (proj (i,n)) . y2 = ry2 ) by PDIFF_1:def 1;
(proj (i,n)) . (y1 + y2) = (proj (i,n)) . (yy1 + yy2) by REAL_NS1:2
.= (yy1 + yy2) . i by PDIFF_1:def 1
.= ry1 + ry2 by RVSUM_1:11 ;
hence (proj (i,n)) . (y1 + y2) = ((proj (i,n)) . y1) + ((proj (i,n)) . y2) by A1; :: thesis: verum