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 G1 * (idt F1) = idt (G1 * F1)
let F1 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C holds G1 * (idt F1) = idt (G1 * F1)
let G1 be covariant Functor of B,C; :: thesis: G1 * (idt F1) = idt (G1 * F1)

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

let a be Object of A; :: thesis: (G1 * (idt F1)) ! a = (idt (G1 * F1)) ! a
thus (G1 * (idt F1)) ! a = G1 . ((idt F1) ! a) by Th11
.= G1 . (idm (F1 . a)) by FUNCTOR2:4
.= idm (G1 . (F1 . a)) by FUNCTOR2:1
.= idm ((G1 * F1) . a) by FUNCTOR0:33
.= (idt (G1 * F1)) ! a by FUNCTOR2:4 ; :: thesis: verum

end;

hence G1 * (idt F1) = idt (G1 * F1) by FUNCTOR2:3; :: thesis: verum