theorem Th25: :: FUNCTOR0:25

for C1 being non empty AltGraph
for C2 being non empty reflexive AltGraph
for o2 being Object of C2
for m being Morphism of o2,o2
for F being feasible Covariant FunctorStr over C1,C2 st F = C1 --> m holds
for o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
F . f = m