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

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