let A be category; ex F, G being covariant Functor of A,A st
( G * F, id A are_naturally_equivalent & F * G, id A are_naturally_equivalent )
take
id A
; ex G being covariant Functor of A,A st
( G * (id A), id A are_naturally_equivalent & (id A) * G, id A are_naturally_equivalent )
take
id A
; ( (id A) * (id A), id A are_naturally_equivalent & (id A) * (id A), id A are_naturally_equivalent )
thus
( (id A) * (id A), id A are_naturally_equivalent & (id A) * (id A), id A are_naturally_equivalent )
by FUNCTOR3:4; verum