:: deftheorem defines (#) INTEGR15:def 11 :
for n being Nat
for r being Real
for Z being set
for f being PartFunc of Z,(REAL n) holds r (#) f = f [#] r;