let A, B be Category; :: thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
F1 ~= F3
let F1, F2, F3 be Functor of A,B; :: thesis: ( F1 ~= F2 & F2 ~= F3 implies F1 ~= F3 )
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 not F2 ~= F3 or F1 ~= F3 )
given t being natural_transformation of F1,F2 such that A2: t is invertible ; :: thesis: ( not F2 ~= F3 or F1 ~= F3 )
assume A3: F2 is_naturally_transformable_to F3 ; :: according to NATTRA_1:def 11 :: thesis: ( for t being natural_transformation of F2,F3 holds not t is invertible or F1 ~= F3 )
given t' being natural_transformation of F2,F3 such that A4: t' is invertible ; :: thesis: F1 ~= F3
thus F1 is_naturally_transformable_to F3 by A1, A3, Th25; :: according to NATTRA_1:def 11 :: thesis: ex t being natural_transformation of F1,F3 st t is invertible
take t' `*` t ; :: thesis: t' `*` t is invertible
let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (t' `*` t) . a is invertible
A5: (t' `*` t) . a = (t' . a) * (t . a) by A1, A3, Th27;
( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A1, A3, Def7;
then A6: ( Hom (F1 . a),(F2 . a) <> {} & Hom (F2 . a),(F3 . a) <> {} ) by Def2;
( t' . a is invertible & t . a is invertible ) by A2, A4, Def10;
hence (t' `*` t) . a is invertible by A5, A6, CAT_1:75; :: thesis: verum