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

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