thus id A is feasible :: thesis: id A is Covariant

proof

let o1, o2 be Object of A; :: according to FUNCTOR0:def 11 :: thesis: ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} )
A1: [o1,o2] in [: the carrier of A, the carrier of A:] by ZFMISC_1:87;
the ObjectMap of (id A) . (o1,o2) = (id [: the carrier of A, the carrier of A:]) . [o1,o2] by Def29
.= [o1,o2] by A1, FUNCT_1:18 ;
then the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) = the Arrows of A . (o1,o2)
.= <^o1,o2^> by ALTCAT_1:def 1 ;
hence ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (id A) . (o1,o2)) <> {} ) ; :: thesis: verum

end;

thus id A is Covariant :: thesis: verum

proof

take I = id the carrier of A; :: according to FUNCTOR0:def 1,FUNCTOR0:def 12 :: thesis: the ObjectMap of (id A) = [:I,I:]
thus the ObjectMap of (id A) = id [: the carrier of A, the carrier of A:] by Def29
.= [:I,I:] by FUNCT_3:69 ; :: thesis: verum

end;