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

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

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

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

then A2: F1 is_transformable_to F2 by Def4;

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

(e ") " = e

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

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

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

then A2: F1 is_transformable_to F2 by Def4;

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

hence
(e ") " = e
by A2, FUNCTOR2:3; :: thesis: verumlet a be Object of A; :: thesis: ((e ") ") ! a = e ! a

A3: <^(F1 . a),(F2 . a)^> <> {} by A2;

F2 is_transformable_to F1 by A1;

then A4: <^(F2 . a),(F1 . a)^> <> {} ;

e ! a is iso by A1, Def5;

then A5: ( e ! a is retraction & e ! a is coretraction ) by ALTCAT_3:5;

thus ((e ") ") ! a = ((e ") ! a) " by A1, Th38

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

.= e ! a by A3, A4, A5, ALTCAT_3:3 ; :: thesis: verum

end;A3: <^(F1 . a),(F2 . a)^> <> {} by A2;

F2 is_transformable_to F1 by A1;

then A4: <^(F2 . a),(F1 . a)^> <> {} ;

e ! a is iso by A1, Def5;

then A5: ( e ! a is retraction & e ! a is coretraction ) by ALTCAT_3:5;

thus ((e ") ") ! a = ((e ") ! a) " by A1, Th38

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

.= e ! a by A3, A4, A5, ALTCAT_3:3 ; :: thesis: verum