let F be Functor of A,B; ( F is_transformable_to F & ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) )
ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a)
hence
( F is_transformable_to F & ex t being transformation of F,F st
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F /. f) = (F /. f) * (t . a) )
; verum