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

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 Th29
.= id (G . (F . a)) by NATTRA_1:21
.= id ((G * F) . a) by CAT_1:113
.= (id (G * F)) . a by NATTRA_1:21 ; :: thesis: verum

end;

hence (id G) * F = id (G * F) by Th31; :: thesis: verum