theorem Th30: :: FUNCTOR0:30

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