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