theorem :: FUNCTOR1:21

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