theorem Th17: :: ALTCAT_4:17

for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr over C1,C2
for o1, o2 being Object of C1
for Fm being Morphism of (F . o2),(F . o1) st <^o1,o2^> <> {} & F is full & F is feasible holds
ex m being Morphism of o1,o2 st Fm = F . m