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

let a be Object of B; :: thesis: t . a = (id F) . a
( t . a in Hom (F . a),(F . a) & Hom (F . a),(F . a) = {(id (F . a))} ) by Th3, Th44;
hence t . a = id (F . a) by TARSKI:def 1
.= (id F) . a by Th21 ;
:: thesis: verum

end;

hence t = id F by Th20; :: thesis: verum