( F is_naturally_transformable_to F & ( for a, b being object of st <^a,b^> <> {} holds
for f being Morphism of , holds ((idt F) ! b) * (F . f) = (F . f) * ((idt F) ! a) ) ) by Lm1, Th9;
hence idt F is natural_transformation of F,F by Def7; :: thesis: verum