theorem Th8: :: PDIFF_9:8

for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for r being Real holds <>* (r (#) f) = r (#) (<>* f)