let A, B, C be Category; :: thesis: for F being Functor of A,B
for G being Functor of B,C holds G * (id F) = id (G * F)
let F be Functor of A,B; :: thesis: for G being Functor of B,C holds G * (id F) = id (G * F)
let G be Functor of B,C; :: thesis: G * (id F) = id (G * F)

now :: thesis: for a being Object of A holds (G * (id F)) . a = (id (G * F)) . a

let a be Object of A; :: thesis: (G * (id F)) . a = (id (G * F)) . a
thus (G * (id F)) . a = G /. ((id F) . a) by Th21
.= G /. (id (F . a)) by NATTRA_1:20
.= id (G . (F . a)) by NATTRA_1:15
.= id ((G * F) . a) by CAT_1:76
.= (id (G * F)) . a by NATTRA_1:20 ; :: thesis: verum

end;

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