let A, B be category; :: thesis: for F1 being covariant Functor of A,B holds (idt F1) " = idt F1
let F1 be covariant Functor of A,B; :: thesis: (idt F1) " = idt F1
now :: thesis: for a being Object of A holds ((idt F1) ") ! a = (idt F1) ! a
let a be Object of A; :: thesis: ((idt F1) ") ! a = (idt F1) ! a
thus ((idt F1) ") ! a = ((idt F1) ! a) " by Th38
.= (idm (F1 . a)) " by FUNCTOR2:4
.= idm (F1 . a) by ALTCAT_3:4
.= (idt F1) ! a by FUNCTOR2:4 ; :: thesis: verum
end;
hence (idt F1) " = idt F1 by FUNCTOR2:3; :: thesis: verum