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)

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

hence
G1 * (idt F1) = idt (G1 * F1)
by FUNCTOR2:3; :: thesis: verumlet 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;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