let n be non zero Element of NAT ; :: thesis: for x, y being Element of REAL n
for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
let x, y be Element of REAL n; :: thesis: for i being Element of NAT holds (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
let i be Element of NAT ; :: thesis: (proj (i,n)) . (x + y) = ((proj (i,n)) . x) + ((proj (i,n)) . y)
thus (proj (i,n)) . (x + y) = (x + y) . i by PDIFF_1:def 1
.= (x . i) + (y . i) by RVSUM_1:11
.= ((proj (i,n)) . x) + (y . i) by PDIFF_1:def 1
.= ((proj (i,n)) . x) + ((proj (i,n)) . y) by PDIFF_1:def 1 ; :: thesis: verum