theorem Th39: :: FUNCTOR0:39

for A, B being non empty transitive with_units AltCatStr
for F being feasible FunctorStr over A,B st F is bijective & F is Contravariant holds
F " is Contravariant