:: deftheorem Def34 defines oneone FOMODEL0:def 34 :
for P being Relation holds
( P is oneone iff P ~ is Function-like );