theorem :: RFUNCT_2:50

for g, p being Real
for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds
h | [.p,g.] is one-to-one