:: deftheorem Def5 defines " FUNCT_1:def 5 :
for f being Function st f is one-to-one holds
f " = f ~ ;