:: deftheorem Def29 defines id FUNCTOR0:def 29 :
for A being AltGraph
for b₂ being strict FunctorStr over A,A holds
( b₂ = id A iff ( the ObjectMap of b₂ = id [: the carrier of A, the carrier of A:] & the MorphMap of b₂ = id the Arrows of A ) );