:: deftheorem defines one-to-one FUNCTOR0:def 6 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is one-to-one iff the ObjectMap of F is one-to-one );