theorem Th1: :: YELLOW20:1

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is coreflexive & F is bijective holds
for a being Object of A
for b being Object of B holds
( F . a = b iff (F ") . b = a )