let A, B be Category; :: thesis: for F1, F2, F3 being Functor of A,B st F1 ~= F2 & F2 ~= F3 holds
for t being natural_equivalence of F1,F2
for t' being natural_equivalence of F2,F3 holds t' `*` t is natural_equivalence of F1,F3
let F1, F2, F3 be Functor of A,B; :: thesis: ( F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2
for t' being natural_equivalence of F2,F3 holds t' `*` t is natural_equivalence of F1,F3 )
assume that
A1: F1,F2 are_naturally_equivalent and
A2: F2,F3 are_naturally_equivalent ; :: thesis: for t being natural_equivalence of F1,F2
for t' being natural_equivalence of F2,F3 holds t' `*` t is natural_equivalence of F1,F3
let t be natural_equivalence of F1,F2; :: thesis: for t' being natural_equivalence of F2,F3 holds t' `*` t is natural_equivalence of F1,F3
let t' be natural_equivalence of F2,F3; :: thesis: t' `*` t is natural_equivalence of F1,F3
thus F1,F3 are_naturally_equivalent by A1, A2, Th32; :: according to NATTRA_1:def 14 :: thesis: t' `*` t is invertible
let a be Object of A; :: according to NATTRA_1:def 10 :: thesis: (t' `*` t) . a is invertible
A3: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A1, A2, Def11;
then A4: (t' `*` t) . a = (t' . a) * (t . a) by Th27;
( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A3, Def7;
then A5: ( Hom (F1 . a),(F2 . a) <> {} & Hom (F2 . a),(F3 . a) <> {} ) by Def2;
( t' is invertible & t is invertible ) by A1, A2, Def14;
then ( t' . a is invertible & t . a is invertible ) by Def10;
hence (t' `*` t) . a is invertible by A4, A5, CAT_1:75; :: thesis: verum