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