theorem :: RFUNCT_2:35

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