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

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

hence
(idt F1) " = idt F1
by FUNCTOR2:3; :: thesis: verumlet 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;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