let A, B be category; :: thesis: for F1, F2, F3 being covariant Functor of A,B

for e being natural_equivalence of F1,F2

for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let F1, F2, F3 be covariant Functor of A,B; :: thesis: for e being natural_equivalence of F1,F2

for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let e be natural_equivalence of F1,F2; :: thesis: for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let e1 be natural_equivalence of F2,F3; :: thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1,F3 )

assume that

A1: F1,F2 are_naturally_equivalent and

A2: F2,F3 are_naturally_equivalent ; :: thesis: e1 `*` e is natural_equivalence of F1,F3

thus A3: F1,F3 are_naturally_equivalent by A1, A2, Th33; :: according to FUNCTOR3:def 5 :: thesis: for a being Object of A holds (e1 `*` e) ! a is iso

let a be Object of A; :: thesis: (e1 `*` e) ! a is iso

A4: F1 is_transformable_to F2 by A1, Def4;

then A5: <^(F1 . a),(F2 . a)^> <> {} ;

F3 is_transformable_to F1 by A3;

then A6: <^(F3 . a),(F1 . a)^> <> {} ;

A7: F2 is_transformable_to F3 by A2, Def4;

then A8: <^(F2 . a),(F3 . a)^> <> {} ;

( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A1, A2;

then A9: (e1 `*` e) ! a = (e1 `*` e) ! a by FUNCTOR2:def 8

.= (e1 ! a) * (e ! a) by A4, A7, FUNCTOR2:def 5 ;

( e1 ! a is iso & e ! a is iso ) by A1, A2, Def5;

hence (e1 `*` e) ! a is iso by A9, A5, A8, A6, ALTCAT_3:7; :: thesis: verum

for e being natural_equivalence of F1,F2

for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let F1, F2, F3 be covariant Functor of A,B; :: thesis: for e being natural_equivalence of F1,F2

for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let e be natural_equivalence of F1,F2; :: thesis: for e1 being natural_equivalence of F2,F3 st F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

e1 `*` e is natural_equivalence of F1,F3

let e1 be natural_equivalence of F2,F3; :: thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies e1 `*` e is natural_equivalence of F1,F3 )

assume that

A1: F1,F2 are_naturally_equivalent and

A2: F2,F3 are_naturally_equivalent ; :: thesis: e1 `*` e is natural_equivalence of F1,F3

thus A3: F1,F3 are_naturally_equivalent by A1, A2, Th33; :: according to FUNCTOR3:def 5 :: thesis: for a being Object of A holds (e1 `*` e) ! a is iso

let a be Object of A; :: thesis: (e1 `*` e) ! a is iso

A4: F1 is_transformable_to F2 by A1, Def4;

then A5: <^(F1 . a),(F2 . a)^> <> {} ;

F3 is_transformable_to F1 by A3;

then A6: <^(F3 . a),(F1 . a)^> <> {} ;

A7: F2 is_transformable_to F3 by A2, Def4;

then A8: <^(F2 . a),(F3 . a)^> <> {} ;

( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A1, A2;

then A9: (e1 `*` e) ! a = (e1 `*` e) ! a by FUNCTOR2:def 8

.= (e1 ! a) * (e ! a) by A4, A7, FUNCTOR2:def 5 ;

( e1 ! a is iso & e ! a is iso ) by A1, A2, Def5;

hence (e1 `*` e) ! a is iso by A9, A5, A8, A6, ALTCAT_3:7; :: thesis: verum