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