let A be discrete Category; :: thesis: for B being Category
for F being Functor of B,A
for t being transformation of F,F holds t = id F
let B be Category; :: thesis: for F being Functor of B,A
for t being transformation of F,F holds t = id F
let F be Functor of B,A; :: thesis: for t being transformation of F,F holds t = id F
let t be transformation of F,F; :: thesis: t = id F
now :: thesis: for a being Object of B holds t . a = (id F) . a
let a be Object of B; :: thesis: t . a = (id F) . a
A1: Hom ((F . a),(F . a)) = {(id (F . a))} by Th33;
t . a in Hom ((F . a),(F . a)) by CAT_1:def 5;
hence t . a = id (F . a) by A1, TARSKI:def 1
.= (id F) . a by Th16 ;
:: thesis: verum
end;
hence t = id F by Th15; :: thesis: verum