theorem Th26: :: FUNCTOR0:26

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