theorem :: FUNCTOR1:19

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 ") * F = id A