theorem Th21: :: FUNCTOR0:21

for C1, C2 being non empty AltGraph
for o2 being Object of C2 st <^o2,o2^> <> {} holds
for m being Morphism of o2,o2
for o1 being Object of C1 holds (C1 --> m) . o1 = o2