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;

A3: now

let i be set ; :: thesis: ( i in [:the carrier of A,the carrier of A:] & the Arrows of A . i <> {} implies the Arrows of B . (the ObjectMap of F . i) <> {} )
assume i in [:the carrier of A,the carrier of A:] ; :: thesis: ( the Arrows of A . i <> {} implies the Arrows of B . (the ObjectMap of F . i) <> {} )
then consider i1, i2 being set such that
A4: ( i1 in the carrier of A & i2 in the carrier of A & [i1,i2] = i ) by ZFMISC_1:def 2;
reconsider i1 = i1, i2 = i2 as object of A by A4;
the Arrows of A . i1,i2 = <^i1,i2^> by ALTCAT_1:def 2;
then ( the Arrows of A . i = <^i1,i2^> & the ObjectMap of F . i = the ObjectMap of F . i1,i2 ) by A4;
hence ( the Arrows of A . i <> {} implies the Arrows of B . (the ObjectMap of F . i) <> {} ) by FUNCTOR0:def 12; :: thesis: verum

end;

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, A3, Lm1 ;
hence (id B) * F = FunctorStr(# the ObjectMap of F,the MorphMap of F #) by A1; :: thesis: verum