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