let A be non empty transitive with_units AltCatStr ; :: thesis: 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 #)
let B be non empty with_units AltCatStr ; :: thesis: for F being feasible FunctorStr over A,B holds F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
let F be feasible FunctorStr over A,B; :: thesis: F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A1: the ObjectMap of (F * (id A)) = the ObjectMap of F * the ObjectMap of (id A) by FUNCTOR0:def 36
.= the ObjectMap of F * (id [: the carrier of A, the carrier of A:]) 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 (F * (id A)) = ( the MorphMap of F * the ObjectMap of (id A)) ** the MorphMap of (id A) by FUNCTOR0:def 36
.= ( the MorphMap of F * (id [: the carrier of A, the carrier of A:])) ** the MorphMap of (id A) by FUNCTOR0:def 29
.= the MorphMap of F ** the MorphMap of (id A) by FUNCTOR0:2
.= the MorphMap of F ** (id the Arrows of A) by FUNCTOR0:def 29
.= the MorphMap of F by A2, MSUALG_3:3 ;
hence F * (id A) = FunctorStr(# the ObjectMap of F, the MorphMap of F #) by A1; :: thesis: verum