let A be non empty transitive AltCatStr ; 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 ; 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; (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; verum