set e = the natural_equivalence of F,F;
the natural_equivalence of F,F `*` ( the natural_equivalence of F,F ") = idt F by Th39;
hence idt F is natural_equivalence of F,F by Th34; :: thesis: verum