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

F1,F3 are_naturally_equivalent

let F1, F2, F3 be covariant Functor of A,B; :: thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies F1,F3 are_naturally_equivalent )

assume that

A1: F1 is_naturally_transformable_to F2 and

A2: F2 is_transformable_to F1 ; :: according to FUNCTOR3:def 4 :: thesis: ( for t being natural_transformation of F1,F2 holds

not for a being Object of A holds t ! a is iso or not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )

given t being natural_transformation of F1,F2 such that A3: for a being Object of A holds t ! a is iso ; :: thesis: ( not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )

assume that

A4: F2 is_naturally_transformable_to F3 and

A5: F3 is_transformable_to F2 ; :: according to FUNCTOR3:def 4 :: thesis: ( for t being natural_transformation of F2,F3 holds

not for a being Object of A holds t ! a is iso or F1,F3 are_naturally_equivalent )

given t1 being natural_transformation of F2,F3 such that A6: for a being Object of A holds t1 ! a is iso ; :: thesis: F1,F3 are_naturally_equivalent

thus ( F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 ) by A1, A2, A4, A5, FUNCTOR2:2, FUNCTOR2:8; :: according to FUNCTOR3:def 4 :: thesis: ex t being natural_transformation of F1,F3 st

for a being Object of A holds t ! a is iso

take t1 `*` t ; :: thesis: for a being Object of A holds (t1 `*` t) ! a is iso

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

A7: t1 ! a is iso by A6;

F3 is_transformable_to F1 by A2, A5, FUNCTOR2:2;

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

A9: t ! a is iso by A3;

A10: F2 is_transformable_to F3 by A4;

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

A12: F1 is_transformable_to F2 by A1;

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

(t1 `*` t) ! a = (t1 `*` t) ! a by A1, A4, FUNCTOR2:def 8

.= (t1 ! a) * (t ! a) by A12, A10, FUNCTOR2:def 5 ;

hence (t1 `*` t) ! a is iso by A13, A11, A8, A7, A9, ALTCAT_3:7; :: thesis: verum

F1,F3 are_naturally_equivalent

let F1, F2, F3 be covariant Functor of A,B; :: thesis: ( F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent implies F1,F3 are_naturally_equivalent )

assume that

A1: F1 is_naturally_transformable_to F2 and

A2: F2 is_transformable_to F1 ; :: according to FUNCTOR3:def 4 :: thesis: ( for t being natural_transformation of F1,F2 holds

not for a being Object of A holds t ! a is iso or not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )

given t being natural_transformation of F1,F2 such that A3: for a being Object of A holds t ! a is iso ; :: thesis: ( not F2,F3 are_naturally_equivalent or F1,F3 are_naturally_equivalent )

assume that

A4: F2 is_naturally_transformable_to F3 and

A5: F3 is_transformable_to F2 ; :: according to FUNCTOR3:def 4 :: thesis: ( for t being natural_transformation of F2,F3 holds

not for a being Object of A holds t ! a is iso or F1,F3 are_naturally_equivalent )

given t1 being natural_transformation of F2,F3 such that A6: for a being Object of A holds t1 ! a is iso ; :: thesis: F1,F3 are_naturally_equivalent

thus ( F1 is_naturally_transformable_to F3 & F3 is_transformable_to F1 ) by A1, A2, A4, A5, FUNCTOR2:2, FUNCTOR2:8; :: according to FUNCTOR3:def 4 :: thesis: ex t being natural_transformation of F1,F3 st

for a being Object of A holds t ! a is iso

take t1 `*` t ; :: thesis: for a being Object of A holds (t1 `*` t) ! a is iso

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

A7: t1 ! a is iso by A6;

F3 is_transformable_to F1 by A2, A5, FUNCTOR2:2;

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

A9: t ! a is iso by A3;

A10: F2 is_transformable_to F3 by A4;

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

A12: F1 is_transformable_to F2 by A1;

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

(t1 `*` t) ! a = (t1 `*` t) ! a by A1, A4, FUNCTOR2:def 8

.= (t1 ! a) * (t ! a) by A12, A10, FUNCTOR2:def 5 ;

hence (t1 `*` t) ! a is iso by A13, A11, A8, A7, A9, ALTCAT_3:7; :: thesis: verum