let C, D be category; :: thesis: for F, F1, F2 being Functor of C,D st F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant holds
F1 is_naturally_transformable_to F2
let F, F1, F2 be Functor of C,D; :: thesis: ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant implies F1 is_naturally_transformable_to F2 )
set T1 = the natural_transformation of F1,F;
set T2 = the natural_transformation of F,F2;
assume ( F1 is_naturally_transformable_to F & F is_naturally_transformable_to F2 & F is covariant & F1 is covariant & F2 is covariant ) ; :: thesis: F1 is_naturally_transformable_to F2
then ex T being natural_transformation of F1,F2 st
( T is_natural_transformation_of F1,F2 & ( for f, f1, f2 being morphism of C st f1 is identity & f2 is identity & f |> f1 & f2 |> f holds
T . f = (( the natural_transformation of F,F2 . f2) (*) (F . f)) (*) ( the natural_transformation of F1,F . f1) ) ) by Lm3;
hence F1 is_naturally_transformable_to F2 ; :: thesis: verum