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
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
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
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
let F2, G2 be Functor of A,C; :: thesis: ( F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 implies for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a) )
assume that
A1: F1 is_naturally_transformable_to G1 and
A2: F2 is_naturally_transformable_to G2 ; :: thesis: for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
let t1 be natural_transformation of F1,G1; :: thesis: for t2 being natural_transformation of F2,G2
for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
let t2 be natural_transformation of F2,G2; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a) )
assume A3: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
A4: Hom ((F1 . a),(F1 . b)) <> {} by A3, CAT_1:84;
let f be Morphism of a,b; :: thesis: (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:G1,G2:> . f) * (<:t1,t2:> . a)
A5: ( (t1 . b) * (F1 . f) = (G1 . f) * (t1 . a) & (t2 . b) * (F2 . f) = (G2 . f) * (t2 . a) ) by A1, A2, A3, NATTRA_1:def 8;
A6: <:G1,G2:> . f = [(G1 . f),(G2 . f)] by A3, Th42;
A7: <:F1,F2:> . f = [(F1 . f),(F2 . f)] by A3, Th42;
A8: F2 is_transformable_to G2 by A2, NATTRA_1:def 7;
then A9: Hom ((F2 . b),(G2 . b)) <> {} by NATTRA_1:def 2;
A10: F1 is_transformable_to G1 by A1, NATTRA_1:def 7;
then A11: <:t1,t2:> . b = [(t1 . b),(t2 . b)] by A8, Th45;
A12: <:t1,t2:> . a = [(t1 . a),(t2 . a)] by A10, A8, Th45;
A13: Hom ((G2 . a),(G2 . b)) <> {} by A3, CAT_1:84;
A14: <:F1,F2:> is_transformable_to <:G1,G2:> by A10, A8, Th44;
then A15: Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) <> {} by NATTRA_1:def 2;
A16: Hom ((<:G1,G2:> . a),(<:G1,G2:> . b)) <> {} by A3, CAT_1:84;
A17: Hom ((G1 . a),(G1 . b)) <> {} by A3, CAT_1:84;
A18: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
then A19: (t2 . b) * (F2 . f) = (t2 . b) * (F2 . f) by A9, CAT_1:def 10;
A20: Hom ((F2 . a),(G2 . a)) <> {} by A8, NATTRA_1:def 2;
then A21: (G2 . f) * (t2 . a) = (G2 . f) * (t2 . a) by A13, CAT_1:def 10;
A22: cod (t2 . a) = G2 . a by A20, CAT_1:5
.= dom (G2 . f) by A13, CAT_1:5 ;
A23: Hom ((F1 . b),(G1 . b)) <> {} by A10, NATTRA_1:def 2;
then A24: dom (t1 . b) = F1 . b by CAT_1:5
.= cod (F1 . f) by A4, CAT_1:5 ;
A25: Hom ((F1 . a),(G1 . a)) <> {} by A10, NATTRA_1:def 2;
then A26: (G1 . f) * (t1 . a) = (G1 . f) * (t1 . a) by A17, CAT_1:def 10;
A27: cod (t1 . a) = G1 . a by A25, CAT_1:5
.= dom (G1 . f) by A17, CAT_1:5 ;
A28: dom (t2 . b) = F2 . b by A9, CAT_1:5
.= cod (F2 . f) by A18, CAT_1:5 ;
A29: (t1 . b) * (F1 . f) = (t1 . b) * (F1 . f) by A23, A4, CAT_1:def 10;
A30: Hom ((<:F1,F2:> . b),(<:G1,G2:> . b)) <> {} by A14, NATTRA_1:def 2;
Hom ((<:F1,F2:> . a),(<:F1,F2:> . b)) <> {} by A3, CAT_1:84;
hence (<:t1,t2:> . b) * (<:F1,F2:> . f) = (<:t1,t2:> . b) * (<:F1,F2:> . f) by A30, CAT_1:def 10
.= [((G1 . f) * (t1 . a)),((G2 . f) * (t2 . a))] by A5, A11, A7, A24, A28, A29, A19, CAT_2:29
.= (<:G1,G2:> . f) * (<:t1,t2:> . a) by A26, A21, A27, A22, A6, A12, CAT_2:29
.= (<:G1,G2:> . f) * (<:t1,t2:> . a) by A15, A16, CAT_1:def 10 ;
:: thesis: verum