:: deftheorem Def4 defines /" TOPS_2:def 4 :
for S, T being set
for f being Function of S,T st f is bijective holds
f /" = f " ;