let A, B be category; for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
F is_naturally_transformable_to F2
let F, F1, F2 be covariant Functor of A,B; ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2 )
assume A1:
F is_transformable_to F1
; FUNCTOR2:def 6 ( for t being transformation of F,F1 ex a, b being Object of A st
( <^a,b^> <> {} & not for f being Morphism of a,b holds (t ! b) * (F . f) = (F1 . f) * (t ! a) ) or not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )
given t1 being transformation of F,F1 such that A2:
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t1 ! b) * (F . f) = (F1 . f) * (t1 ! a)
; ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )
assume A3:
F1 is_transformable_to F2
; FUNCTOR2:def 6 ( for t being transformation of F1,F2 ex a, b being Object of A st
( <^a,b^> <> {} & not for f being Morphism of a,b holds (t ! b) * (F1 . f) = (F2 . f) * (t ! a) ) or F is_naturally_transformable_to F2 )
given t2 being transformation of F1,F2 such that A4:
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t2 ! b) * (F1 . f) = (F2 . f) * (t2 ! a)
; F is_naturally_transformable_to F2
thus
F is_transformable_to F2
by A1, A3, Th2; FUNCTOR2:def 6 ex t being transformation of F,F2 st
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (t ! b) * (F . f) = (F2 . f) * (t ! a)
take
t2 `*` t1
; for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
thus
for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds ((t2 `*` t1) ! b) * (F . f) = (F2 . f) * ((t2 `*` t1) ! a)
by A1, A2, A3, A4, Lm2; verum