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

( 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