let C, D be category; :: thesis: for F being Functor of C,D st F is covariant holds
( F (*) (id C) = F & (id D) (*) F = F )
let F be Functor of C,D; :: thesis: ( F is covariant implies ( F (*) (id C) = F & (id D) (*) F = F ) )
assume A1: F is covariant ; :: thesis: ( F (*) (id C) = F & (id D) (*) F = F )
thus F (*) (id C) = (id C) * F by A1, CAT_6:def 27
.= (id the carrier of C) * F by STRUCT_0:def 4
.= F by FUNCT_2:17 ; :: thesis: (id D) (*) F = F
thus (id D) (*) F = F * (id D) by A1, CAT_6:def 27
.= F * (id the carrier of D) by STRUCT_0:def 4
.= F by FUNCT_2:17 ; :: thesis: verum