theorem Th10: :: FCONT_3:10

for X being set
for f being one-to-one PartFunc of REAL,REAL st f | X is decreasing holds
((f | X) ") | (f .: X) is decreasing