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