let A, B be category; :: thesis: 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; :: thesis: ( 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 ; :: according to FUNCTOR2:def 6 :: thesis: ( 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) ; :: thesis: ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )

assume A3: F1 is_transformable_to F2 ; :: according to FUNCTOR2:def 6 :: thesis: ( 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) ; :: thesis: F is_naturally_transformable_to F2

thus F is_transformable_to F2 by A1, A3, Th2; :: according to FUNCTOR2:def 6 :: thesis: 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 ; :: thesis: 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; :: thesis: verum

F is_naturally_transformable_to F2

let F, F1, F2 be covariant Functor of A,B; :: thesis: ( 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 ; :: according to FUNCTOR2:def 6 :: thesis: ( 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) ; :: thesis: ( not F1 is_naturally_transformable_to F2 or F is_naturally_transformable_to F2 )

assume A3: F1 is_transformable_to F2 ; :: according to FUNCTOR2:def 6 :: thesis: ( 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) ; :: thesis: F is_naturally_transformable_to F2

thus F is_transformable_to F2 by A1, A3, Th2; :: according to FUNCTOR2:def 6 :: thesis: 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 ; :: thesis: 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; :: thesis: verum