theorem Th2: :: YELLOW20:2

for A, B being non empty transitive with_units AltCatStr
for F being feasible Covariant FunctorStr over A,B
for G being feasible Covariant FunctorStr over B,A st F is bijective & G = F " holds
for a1, a2 being Object of A st <^a1,a2^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of (F . a1),(F . a2) holds
( F . f = g iff G . g = f )