let A, B be category; :: thesis: for F1, F3, F2 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, F3, F2 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: ( F3 is_transformable_to F2 & F2 is_transformable_to F1 ) by A2, A3, Def4;
then A6: F3 is_transformable_to F1 by FUNCTOR2:4;
A7: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 ) by A2, A3, Def4;
A8: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A2, A3, Def4;

now

let a be object of A; :: thesis: (k " ) ! a = ((e " ) `*` (e1 " )) ! a
A9: ( e ! a is iso & e1 ! a is iso ) by A2, A3, Def5;
A10: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} & <^(F3 . a),(F1 . a)^> <> {} ) by A6, A8, FUNCTOR2:def 1;
thus (k " ) ! a = ((e1 `*` e) ! a) " by A1, A2, A3, Th33, Th38
.= ((e1 `*` e) ! a) " by A7, FUNCTOR2:def 8
.= ((e1 ! a) * (e ! a)) " by A8, FUNCTOR2:def 5
.= ((e ! a) " ) * ((e1 ! a) " ) by A9, A10, ALTCAT_3:7
.= ((e ! a) " ) * ((e1 " ) ! a) by A3, Th38
.= ((e " ) ! a) * ((e1 " ) ! a) by A2, Th38
.= ((e " ) `*` (e1 " )) ! a by A5, FUNCTOR2:def 5
.= ((e " ) `*` (e1 " )) ! a by A4, FUNCTOR2:def 8 ; :: thesis: verum

end;

hence k " = (e " ) `*` (e1 " ) by A6, FUNCTOR2:5; :: thesis: verum