let n be non zero Element of NAT ; 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; 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); (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; verum