let F be covariant 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 <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a) )
thus F is_transformable_to F ; :: thesis: ex t being transformation of F,F st
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F . f) * (t ! a)
take idt F ; :: thesis: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a)
thus for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) by Lm1; :: thesis: verum