:: deftheorem defines bijective FUNCTOR0:def 35 :
for A, B being AltGraph
for F being FunctorStr over A,B holds
( F is bijective iff ( F is injective & F is surjective ) );