theorem :: RFUNCT_2:29

for X, Y being set
for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds
h | X is decreasing