theorem Th24: :: FUNCTOR0:24

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 o, o9 being Object of C1
for f being Morphism of o,o9 st <^o,o9^> <> {} holds
(Morph-Map ((C1 --> m),o,o9)) . f = m