theorem :: INTEGR15:23

for n being Nat
for Z, x being set
for f being PartFunc of Z,(REAL n)
for r being Real st x in dom (r (#) f) holds
(r (#) f) /. x = r * (f /. x)