let C, D be category; :: thesis: for F being Functor of C,D st F is covariant holds
F is_natural_transformation_of F,F
let F be Functor of C,D; :: thesis: ( F is covariant implies F is_natural_transformation_of F,F )
assume A1: F is covariant ; :: thesis: F is_natural_transformation_of F,F
then A2: F is multiplicative by CAT_6:def 25;
for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f1 |> f & f |> f2 holds
( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) )

proof

let f, f1, f2 be morphism of C; :: thesis: ( f1 is identity & f2 is identity & f1 |> f & f |> f2 implies ( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) ) )
assume A3: f1 is identity ; :: thesis: ( not f2 is identity or not f1 |> f or not f |> f2 or ( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) ) )
assume A4: f2 is identity ; :: thesis: ( not f1 |> f or not f |> f2 or ( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) ) )
assume A5: f1 |> f ; :: thesis: ( not f |> f2 or ( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) ) )
assume A6: f |> f2 ; :: thesis: ( F . f1 |> F . f & F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) )
thus F . f1 |> F . f by A2, A5, CAT_6:def 23; :: thesis: ( F . f |> F . f2 & F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) )
thus F . f |> F . f2 by A2, A6, CAT_6:def 23; :: thesis: ( F . f = (F . f1) (*) (F . f) & F . f = (F . f) (*) (F . f2) )
thus F . f = F . (f1 (*) f) by A3, A5, CAT_6:def 4, CAT_6:def 14
.= (F . f1) (*) (F . f) by A2, A5, CAT_6:def 23 ; :: thesis: F . f = (F . f) (*) (F . f2)
thus F . f = F . (f (*) f2) by A4, A6, CAT_6:def 5, CAT_6:def 14
.= (F . f) (*) (F . f2) by A2, A6, CAT_6:def 23 ; :: thesis: verum

end;

hence F is_natural_transformation_of F,F by A1, Th58; :: thesis: verum