let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being covariant Functor of A,B
for a being object of A holds (idt F) ! a = idm (F . a)
let F be covariant 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