let A be non empty transitive AltCatStr ; :: thesis: for B being non empty with_units AltCatStr
for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let B be non empty with_units AltCatStr ; :: thesis: for F being feasible FunctorStr over A,B holds (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let F be feasible FunctorStr over A,B; :: thesis: (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A1: the ObjectMap of ((id B) * F) = the ObjectMap of (id B) * the ObjectMap of F by FUNCTOR0:def 36
.= (id [: the carrier of B, the carrier of B:]) * the ObjectMap of F by FUNCTOR0:def 29
.= the ObjectMap of F by FUNCT_2:17 ;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F by FUNCTOR0:def 4;
the MorphMap of ((id B) * F) = ( the MorphMap of (id B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def 36
.= ((id the Arrows of B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def 29
.= the MorphMap of F by A2, Lm1 ;
hence (id B) * F = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; :: thesis: verum