let A, B, C be non empty transitive with_units AltCatStr ; :: thesis: for F1 being covariant Functor of A,B

for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)

let F1 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)

let G1 be covariant Functor of B,C; :: thesis: (idt G1) * F1 = idt (G1 * F1)

for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)

let F1 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C holds (idt G1) * F1 = idt (G1 * F1)

let G1 be covariant Functor of B,C; :: thesis: (idt G1) * F1 = idt (G1 * F1)

now :: thesis: for a being Object of A holds ((idt G1) * F1) ! a = (idt (G1 * F1)) ! a

hence
(idt G1) * F1 = idt (G1 * F1)
by FUNCTOR2:3; :: thesis: verumlet a be Object of A; :: thesis: ((idt G1) * F1) ! a = (idt (G1 * F1)) ! a

thus ((idt G1) * F1) ! a = (idt G1) ! (F1 . a) by Th12

.= idm (G1 . (F1 . a)) by FUNCTOR2:4

.= idm ((G1 * F1) . a) by FUNCTOR0:33

.= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; :: thesis: verum

end;thus ((idt G1) * F1) ! a = (idt G1) ! (F1 . a) by Th12

.= idm (G1 . (F1 . a)) by FUNCTOR2:4

.= idm ((G1 * F1) . a) by FUNCTOR0:33

.= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; :: thesis: verum