let A, B be category; :: thesis: 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; :: thesis: 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; :: thesis: ( F1,F2 are_naturally_equivalent implies (e " ) `*` e = idt F1 )
assume A1: F1,F2 are_naturally_equivalent ; :: thesis: (e " ) `*` e = idt F1
then A2: F1 is_naturally_transformable_to F2 by Def4;
A3: F1 is_transformable_to F2 by A1, Def4;
A4: F2 is_naturally_transformable_to F1 by A1, Def4;
A5: F2 is_transformable_to F1 by A1, Def4;

now

let a be object of A; :: thesis: ((e " ) `*` e) ! a = (idt F1) ! a
A6: e ! a is iso by A1, Def5;
thus ((e " ) `*` e) ! a = ((e " ) `*` e) ! a by A2, A4, FUNCTOR2:def 8
.= ((e " ) ! a) * (e ! a) by A3, A5, FUNCTOR2:def 5
.= ((e ! a) " ) * (e ! a) by A1, Th38
.= idm (F1 . a) by A6, ALTCAT_3:def 5
.= (idt F1) ! a by FUNCTOR2:6 ; :: thesis: verum

end;

hence (e " ) `*` e = idt F1 by FUNCTOR2:5; :: thesis: verum