let A, B be category; for F1, F2 being covariant Functor of A,B
for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
let F1, F2 be covariant Functor of A,B; for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds
(e ") `*` e = idt F1
let e be natural_equivalence of F1,F2; ( F1,F2 are_naturally_equivalent implies (e ") `*` e = idt F1 )
assume A1:
F1,F2 are_naturally_equivalent
; (e ") `*` e = idt F1
then A2:
( F1 is_transformable_to F2 & F2 is_transformable_to F1 )
by Def4;
A3:
( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 )
by A1, Def4;
hence
(e ") `*` e = idt F1
by FUNCTOR2:3; verum