theorem :: FUNCTOR2:7

for A, B being non empty transitive with_units AltCatStr
for F being covariant Functor of A,B holds F is_naturally_transformable_to F ;