theorem :: RFUNCT_2:17

for X being set
for h being one-to-one Function holds (h | X) " = (h ") | (h .: X)