let F be Functor of A,B; :: thesis: ( 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)

proof

take id F ; :: thesis: for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F . f) = (F . f) * ((id F) . a)
thus for a, b being Object of A st Hom a,b <> {} holds
for f being Morphism of a,b holds ((id F) . b) * (F . f) = (F . f) * ((id F) . a) by Lm1; :: thesis: verum

end;

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) ) ; :: thesis: verum