let A be 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 #)
let B be 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 F be feasible FunctorStr over A,B; 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; verum