:: deftheorem Def17 defines --> FUNCTOR0:def 17 :
for C1, C2 being non empty AltGraph
for o being Object of C2 st <^o,o^> <> {} holds
for m being Morphism of o,o
for b₅ being strict FunctorStr over C1,C2 holds
( b₅ = C1 --> m iff ( the ObjectMap of b₅ = [: the carrier of C1, the carrier of C1:] --> [o,o] & the MorphMap of b₅ = { [[o1,o2],(<^o1,o2^> --> m)] where o1, o2 is Object of C1 : verum } ) );