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
A1: Hom ((F . a),(F . a)) = {(id (F . a))} by Th44;
t . a in Hom ((F . a),(F . a)) by Th3;
hence t . a = id (F . a) by A1, TARSKI:def 1
.= (id F) . a by Th21 ;
:: thesis: verum

end;

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