theorem Th16: :: ALTCAT_4:16

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