let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of B,C holds (id G) * F = id (G * F)
let F be Functor of A,B; :: thesis: for G being Functor of B,C holds (id G) * F = id (G * F)
let G be Functor of B,C; :: thesis: (id G) * F = id (G * F)
now :: thesis: for a being Object of A holds ((id G) * F) . a = (id (G * F)) . a
let a be Object of A; :: thesis: ((id G) * F) . a = (id (G * F)) . a
thus ((id G) * F) . a = (id G) . (F . a) by Th22
.= id (G . (F . a)) by NATTRA_1:20
.= id ((G * F) . a) by CAT_1:76
.= (id (G * F)) . a by NATTRA_1:20 ; :: thesis: verum
end;
hence (id G) * F = id (G * F) by Th24; :: thesis: verum