theorem :: PARTFUN1:38

for X, Y being set
for f being Function st f is one-to-one holds
<:f,X,Y:> " = <:(f "),Y,X:>