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