let C be with_identities CategoryStr ; :: thesis: ex F, G being Functor of C,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id C )
set F = id C;
set G = id C;
A1: ( id C = id the carrier of C & id C = id the carrier of C ) by STRUCT_0:def 4;
take id C ; :: thesis: ex G being Functor of C,C st
( id C is covariant & G is covariant & G (*) (id C) = id C & (id C) (*) G = id C )
take id C ; :: thesis: ( id C is covariant & id C is covariant & (id C) (*) (id C) = id C & (id C) (*) (id C) = id C )
(id C) (*) (id C) = (id the carrier of C) * (id the carrier of C) by A1, Def27
.= id ( the carrier of C /\ the carrier of C) by FUNCT_1:22
.= id C by STRUCT_0:def 4 ;
hence ( id C is covariant & id C is covariant & (id C) (*) (id C) = id C & (id C) (*) (id C) = id C ) ; :: thesis: verum