let F be Functor of C1,C2; :: thesis: F is covariant
A1: for f being morphism of C1 st f is identity holds
F . f is identity

proof

let f be morphism of C1; :: thesis: ( f is identity implies F . f is identity )
assume f is identity ; :: thesis: F . f is identity
A2: F . f = the Object of C2 by CAT_6:def 21;

per cases ( C2 is empty or not C2 is empty ) ;

suppose C2 is empty ; :: thesis: F . f is identity

hence F . f is identity by CAT_6:10; :: thesis: verum

end;

suppose not C2 is empty ; :: thesis: F . f is identity

hence F . f is identity by A2, CAT_6:22; :: thesis: verum

end;

end;

end;

for f1, f2 being morphism of C1 st f1 |> f2 holds
( F . f1 |> F . f2 & F . (f1 (*) f2) = (F . f1) (*) (F . f2) ) by CAT_6:1;
then F is multiplicative by CAT_6:def 23;
hence F is covariant by A1, CAT_6:def 25, CAT_6:def 22; :: thesis: verum