theorem Th31: :: FUNCTOR0:31

for A being non empty AltGraph
for o1, o2 being Object of A st <^o1,o2^> <> {} holds
for F being feasible Covariant FunctorStr over A,A st F = id A holds
for m being Morphism of o1,o2 holds F . m = m