:: deftheorem Def38 defines " FUNCTOR0:def 38 :
for A, B being non empty AltGraph
for F being FunctorStr over A,B st F is bijective holds
for b₄ being strict FunctorStr over B,A holds
( b₄ = F " iff ( the ObjectMap of b₄ = the ObjectMap of F " & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & the MorphMap of b₄ = (f "") * ( the ObjectMap of F ") ) ) );