for r being Real
for X being set
for f, F being PartFunc of REAL,REAL st F is_integral_of f,X holds
r (#) F is_integral_of r (#) f,X