theorem :: RFUNCT_2:33

for Y being set
for r being Real
for h being PartFunc of REAL,REAL holds
( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) )