let A be non empty transitive AltCatStr ; :: thesis: for B being non empty with_units AltCatStr
for F being feasible FunctorStr of 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 of A,B holds (id B) * F = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
let F be feasible FunctorStr of 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 37
.= (id [:the carrier of B,the carrier of B:]) * the ObjectMap of F by FUNCTOR0:def 30
.= the ObjectMap of F by FUNCT_2:23 ;
A2: the MorphMap of F is ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F by FUNCTOR0:def 5;
the MorphMap of ((id B) * F) = (the MorphMap of (id B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def 37
.= ((id the Arrows of B) * the ObjectMap of F) ** the MorphMap of F by FUNCTOR0:def 30
.= the MorphMap of F by A2, Lm1 ;
hence (id B) * F = FunctorStr(# the ObjectMap of F,the MorphMap of F #) by A1; :: thesis: verum