theorem Th16: :: INTEGR15:16

for Z being set
for n, i being Element of NAT
for r being Real
for f being PartFunc of Z,(REAL n) holds (proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f)