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

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