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 t9 being natural_equivalence of F2,F3 holds t9 `*` 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 t9 being natural_equivalence of F2,F3 holds t9 `*` 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 t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

let t be natural_equivalence of F1,F2; :: thesis: for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

let t9 be natural_equivalence of F2,F3; :: thesis: t9 `*` t is natural_equivalence of F1,F3

thus F1,F3 are_naturally_equivalent by A1, A2, Th25; :: according to NATTRA_1:def 14 :: thesis: t9 `*` t is invertible

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

t9 is invertible by A2, Def13;

then A3: t9 . a is invertible ;

t is invertible by A1, Def13;

then A4: t . a is invertible ;

A5: F1 is_naturally_transformable_to F2 by A1;

A6: F2 is_naturally_transformable_to F3 by A2;

(t9 `*` t) . a = (t9 . a) * (t . a) by A5, A6, Th21;

hence (t9 `*` t) . a is invertible by A3, A4, CAT_1:45; :: thesis: verum

for t being natural_equivalence of F1,F2

for t9 being natural_equivalence of F2,F3 holds t9 `*` 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 t9 being natural_equivalence of F2,F3 holds t9 `*` 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 t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

let t be natural_equivalence of F1,F2; :: thesis: for t9 being natural_equivalence of F2,F3 holds t9 `*` t is natural_equivalence of F1,F3

let t9 be natural_equivalence of F2,F3; :: thesis: t9 `*` t is natural_equivalence of F1,F3

thus F1,F3 are_naturally_equivalent by A1, A2, Th25; :: according to NATTRA_1:def 14 :: thesis: t9 `*` t is invertible

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

t9 is invertible by A2, Def13;

then A3: t9 . a is invertible ;

t is invertible by A1, Def13;

then A4: t . a is invertible ;

A5: F1 is_naturally_transformable_to F2 by A1;

A6: F2 is_naturally_transformable_to F3 by A2;

(t9 `*` t) . a = (t9 . a) * (t . a) by A5, A6, Th21;

hence (t9 `*` t) . a is invertible by A3, A4, CAT_1:45; :: thesis: verum