let A, B be category; 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; 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; 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; ( 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
; e1 `*` e is natural_equivalence of F1,F3
thus A3:
F1,F3 are_naturally_equivalent
by A1, A2, Th33; FUNCTOR3:def 5 for a being Object of A holds (e1 `*` e) ! a is iso
let a be Object of A; (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; verum