theorem Th4: :: CFUNCT_1:4
for C being non empty set
for f being PartFunc of C,COMPLEX
for r being Complex holds
( dom (r (#) f) = dom f & ( for c being Element of C st c in dom (r (#) f) holds
(r (#) f) /. c = r * (f /. c) ) )