theorem :: RFUNCT_1:57

for C being non empty set
for c being Element of C
for r being Real
for f being PartFunc of C,REAL st f is total holds
(r (#) f) . c = r * (f . c)