theorem :: GLIB_009:5

for f being one-to-one Function
for X being set holds
( (f | X) " = X |` (f ") & (X |` f) " = (f ") | X )