theorem :: RFUNCT_2:26

for Y being set
for h being PartFunc of REAL,REAL st Y misses dom h holds
( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )