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

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

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

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

let e be natural_equivalence of F1,F2; :: thesis: for e1 being natural_equivalence of F2,F3

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

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

k " = (e ") `*` (e1 ")

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

assume that

A1: k = e1 `*` e and

A2: F1,F2 are_naturally_equivalent and

A3: F2,F3 are_naturally_equivalent ; :: thesis: k " = (e ") `*` (e1 ")

A4: ( F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A2, A3, Def4;

A5: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A2, A3, Def4;

A6: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A2, A3;

A7: ( F3 is_transformable_to F2 & F2 is_transformable_to F1 ) by A2, A3;

then A8: F3 is_transformable_to F1 by FUNCTOR2:2;

for e being natural_equivalence of F1,F2

for e1 being natural_equivalence of F2,F3

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

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

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

let e be natural_equivalence of F1,F2; :: thesis: for e1 being natural_equivalence of F2,F3

for k being natural_equivalence of F1,F3 st k = e1 `*` e & F1,F2 are_naturally_equivalent & F2,F3 are_naturally_equivalent holds

k " = (e ") `*` (e1 ")

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

k " = (e ") `*` (e1 ")

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

assume that

A1: k = e1 `*` e and

A2: F1,F2 are_naturally_equivalent and

A3: F2,F3 are_naturally_equivalent ; :: thesis: k " = (e ") `*` (e1 ")

A4: ( F3 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F1 ) by A2, A3, Def4;

A5: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A2, A3, Def4;

A6: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A2, A3;

A7: ( F3 is_transformable_to F2 & F2 is_transformable_to F1 ) by A2, A3;

then A8: F3 is_transformable_to F1 by FUNCTOR2:2;

now :: thesis: for a being Object of A holds (k ") ! a = ((e ") `*` (e1 ")) ! a

hence
k " = (e ") `*` (e1 ")
by A7, FUNCTOR2:2, FUNCTOR2:3; :: thesis: verumlet a be Object of A; :: thesis: (k ") ! a = ((e ") `*` (e1 ")) ! a

A9: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A5;

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

A11: ( e ! a is iso & e1 ! a is iso ) by A2, A3, Def5;

thus (k ") ! a = ((e1 `*` e) ! a) " by A1, A2, A3, Th33, Th38

.= ((e1 `*` e) ! a) " by A6, FUNCTOR2:def 8

.= ((e1 ! a) * (e ! a)) " by A5, FUNCTOR2:def 5

.= ((e ! a) ") * ((e1 ! a) ") by A11, A9, A10, ALTCAT_3:7

.= ((e ! a) ") * ((e1 ") ! a) by A3, Th38

.= ((e ") ! a) * ((e1 ") ! a) by A2, Th38

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

.= ((e ") `*` (e1 ")) ! a by A4, FUNCTOR2:def 8 ; :: thesis: verum

end;A9: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A5;

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

A11: ( e ! a is iso & e1 ! a is iso ) by A2, A3, Def5;

thus (k ") ! a = ((e1 `*` e) ! a) " by A1, A2, A3, Th33, Th38

.= ((e1 `*` e) ! a) " by A6, FUNCTOR2:def 8

.= ((e1 ! a) * (e ! a)) " by A5, FUNCTOR2:def 5

.= ((e ! a) ") * ((e1 ! a) ") by A11, A9, A10, ALTCAT_3:7

.= ((e ! a) ") * ((e1 ") ! a) by A3, Th38

.= ((e ") ! a) * ((e1 ") ! a) by A2, Th38

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

.= ((e ") `*` (e1 ")) ! a by A4, FUNCTOR2:def 8 ; :: thesis: verum