theorem Th5: :: FUNCTOR1:5

for A, B being non empty AltCatStr
for F being FunctorStr over A,B st F is bijective holds
( the ObjectMap of F is bijective & the MorphMap of F is "1-1" )