:: deftheorem defines -one-to-one FOMODEL0:def 1 :
for X being set
for f being Function holds
( f is X -one-to-one iff f | X is one-to-one );