theorem :: FUNCTOR1:20

for A, B being non empty transitive with_units reflexive AltCatStr
for F being feasible FunctorStr over A,B st F is bijective holds
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)