let A, B be Category; :: thesis: for F, F1, F2 being 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 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 NATTRA_1:def 7 :: thesis: ( for t being transformation of F,F1 ex a, b being Object of A st
( Hom (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 Hom (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 NATTRA_1:def 7 :: thesis: ( for t being transformation of F1,F2 ex a, b being Object of A st
( Hom (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 Hom (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, Th14; :: according to NATTRA_1:def 7 :: thesis: ex t being transformation of F,F2 st
for a, b being Object of A st Hom (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 Hom (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 Hom (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