let A, B be Category; :: thesis: for F1, F2 being Functor of A,B st F1 ~= F2 holds

F2 ~= F1

let F1, F2 be Functor of A,B; :: thesis: ( F1 ~= F2 implies F2 ~= F1 )

assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def 11 :: thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or F2 ~= F1 )

given t being natural_transformation of F1,F2 such that A2: t is invertible ; :: thesis: F2 ~= F1

thus F2 is_naturally_transformable_to F1 by A1, A2, Lm5; :: according to NATTRA_1:def 11 :: thesis: ex t being natural_transformation of F2,F1 st t is invertible

take t " ; :: thesis: t " is invertible

let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (t ") . a is invertible

(t ") . a = (t . a) " by A1, A2, Th23;

hence (t ") . a is invertible by A2, CAT_1:46; :: thesis: verum

F2 ~= F1

let F1, F2 be Functor of A,B; :: thesis: ( F1 ~= F2 implies F2 ~= F1 )

assume A1: F1 is_naturally_transformable_to F2 ; :: according to NATTRA_1:def 11 :: thesis: ( for t being natural_transformation of F1,F2 holds not t is invertible or F2 ~= F1 )

given t being natural_transformation of F1,F2 such that A2: t is invertible ; :: thesis: F2 ~= F1

thus F2 is_naturally_transformable_to F1 by A1, A2, Lm5; :: according to NATTRA_1:def 11 :: thesis: ex t being natural_transformation of F2,F1 st t is invertible

take t " ; :: thesis: t " is invertible

let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (t ") . a is invertible

(t ") . a = (t . a) " by A1, A2, Th23;

hence (t ") . a is invertible by A2, CAT_1:46; :: thesis: verum