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;

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

let 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;

hence k " = (e ") `*` (e1 ") by A7, FUNCTOR2:2, FUNCTOR2:3; :: thesis: verum