theorem :: FUNCTOR3:5

for A being non empty transitive with_units AltCatStr
for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)