theorem Th47: :: FUNCTOR0:47

for C1 being non empty transitive with_units AltCatStr
for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive by Th45;