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