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 F2

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 F2

let e be natural_equivalence of F1,F2; :: thesis: ( F1,F2 are_naturally_equivalent implies e `*` (e ") = idt F2 )

assume A1: F1,F2 are_naturally_equivalent ; :: thesis: e `*` (e ") = idt F2

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;

for e being natural_equivalence of F1,F2 st F1,F2 are_naturally_equivalent holds

e `*` (e ") = idt F2

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 F2

let e be natural_equivalence of F1,F2; :: thesis: ( F1,F2 are_naturally_equivalent implies e `*` (e ") = idt F2 )

assume A1: F1,F2 are_naturally_equivalent ; :: thesis: e `*` (e ") = idt F2

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;

now :: thesis: for a being Object of A holds (e `*` (e ")) ! a = (idt F2) ! a

hence
e `*` (e ") = idt F2
by FUNCTOR2:3; :: thesis: verumlet a be Object of A; :: thesis: (e `*` (e ")) ! a = (idt F2) ! a

A4: e ! a is iso by A1, Def5;

thus (e `*` (e ")) ! a = (e `*` (e ")) ! a by A3, FUNCTOR2:def 8

.= (e ! a) * ((e ") ! a) by A2, FUNCTOR2:def 5

.= (e ! a) * ((e ! a) ") by A1, Th38

.= idm (F2 . a) by A4, ALTCAT_3:def 5

.= (idt F2) ! a by FUNCTOR2:4 ; :: thesis: verum

end;A4: e ! a is iso by A1, Def5;

thus (e `*` (e ")) ! a = (e `*` (e ")) ! a by A3, FUNCTOR2:def 8

.= (e ! a) * ((e ") ! a) by A2, FUNCTOR2:def 5

.= (e ! a) * ((e ! a) ") by A1, Th38

.= idm (F2 . a) by A4, ALTCAT_3:def 5

.= (idt F2) ! a by FUNCTOR2:4 ; :: thesis: verum