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
F1 is_transformable_to F2 by A1, Def7;
then A3: Hom (F1 . a),(F2 . a) <> {} by Def2;
( t . a is invertible & (t " ) . a = (t . a) " ) by A1, A2, Def10, Th30;
hence (t " ) . a is invertible by A3, CAT_1:76; :: thesis: verum