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:27
.= ((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