( F is_naturally_transformable_to F & ( 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;
hence idt F is natural_transformation of F,F by Def7; :: thesis: verum