let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being Functor of A,B
for a being Object of A holds (idt F) ! a = idm (F . a)
let F be Functor of A,B; :: thesis: for a being Object of A holds (idt F) ! a = idm (F . a)
let a be Object of A; :: thesis: (idt F) ! a = idm (F . a)
thus (idt F) ! a = (idt F) . a by Def4
.= idm (F . a) by Def3 ; :: thesis: verum