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)
now :: thesis: for a being Object of A holds ((idt G1) * F1) ! a = (idt (G1 * F1)) ! a
let 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;
hence (idt G1) * F1 = idt (G1 * F1) by FUNCTOR2:3; :: thesis: verum