let A be category; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( (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; :: thesis: verum