let A, B, C be Category; :: thesis: for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>
let F1, G1 be Functor of A,B; :: thesis: for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
<:F1,F2:> is_naturally_transformable_to <:G1,G2:>
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies <:F1,F2:> is_naturally_transformable_to <:G1,G2:> )
assume A1: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 ) ; :: thesis: <:F1,F2:> is_naturally_transformable_to <:G1,G2:>
( F1 is_transformable_to G1 & F2 is_transformable_to G2 ) by A1;
hence <:F1,F2:> is_transformable_to <:G1,G2:> by Th34; :: according to NATTRA_1:def 7 :: thesis: ex b₁ being transformation of <:F1,F2:>,<:G1,G2:> st
for b₂, b₃ being Element of the carrier of A holds
( Hom (b₂,b₃) = {} or for b₄ being Morphism of b₂,b₃ holds (b₁ . b₃) * (<:F1,F2:> /. b₄) = (<:G1,G2:> /. b₄) * (b₁ . b₂) )
set t1 = the natural_transformation of F1,G1;
set t2 = the natural_transformation of F2,G2;
take <: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> ; :: thesis: for b₁, b₂ being Element of the carrier of A holds
( Hom (b₁,b₂) = {} or for b₃ being Morphism of b₁,b₂ holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b₂) * (<:F1,F2:> /. b₃) = (<:G1,G2:> /. b₃) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b₁) )
thus for b₁, b₂ being Element of the carrier of A holds
( Hom (b₁,b₂) = {} or for b₃ being Morphism of b₁,b₂ holds (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b₂) * (<:F1,F2:> /. b₃) = (<:G1,G2:> /. b₃) * (<: the natural_transformation of F1,G1, the natural_transformation of F2,G2:> . b₁) ) by A1, Lm4; :: thesis: verum