for C, D being category
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