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 /. f = G1 . f & G2 /. f = G2 . f ) by A3, CAT_3:def 10;
A7: <:G1,G2:> /. f = <:G1,G2:> . f by A3, CAT_3:def 10
.= [(G1 /. f),(G2 /. f)] by A6, A3, Th32 ;
A8: ( F1 /. f = F1 . f & F2 /. f = F2 . f ) by A3, CAT_3:def 10;
A9: <:F1,F2:> /. f = <:F1,F2:> . f by A3, CAT_3:def 10
.= [(F1 /. f),(F2 /. f)] by A3, Th32, A8 ;
A10: F2 is_transformable_to G2 by A2;
then A11: Hom ((F2 . b),(G2 . b)) <> {} ;
A12: F1 is_transformable_to G1 by A1;
then A13: <:t1,t2:> . b = [(t1 . b),(t2 . b)] by A10, Th35;
A14: <:t1,t2:> . a = [(t1 . a),(t2 . a)] by A12, A10, Th35;
A15: Hom ((G2 . a),(G2 . b)) <> {} by A3, CAT_1:84;
A16: <:F1,F2:> is_transformable_to <:G1,G2:> by A12, A10, Th34;
then A17: Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) <> {} ;
A18: Hom ((<:G1,G2:> . a),(<:G1,G2:> . b)) <> {} by A3, CAT_1:84;
A19: Hom ((G1 . a),(G1 . b)) <> {} by A3, CAT_1:84;
A20: Hom ((F2 . a),(F2 . b)) <> {} by A3, CAT_1:84;
then A21: (t2 . b) * (F2 /. f) = (t2 . b) (*) (F2 /. f) by A11, CAT_1:def 13;
A22: Hom ((F2 . a),(G2 . a)) <> {} by A10;
then A23: (G2 /. f) * (t2 . a) = (G2 /. f) (*) (t2 . a) by A15, CAT_1:def 13;
A24: cod (t2 . a) = G2 . a by A22, CAT_1:5
.= dom (G2 /. f) by A15, CAT_1:5 ;
A25: Hom ((F1 . b),(G1 . b)) <> {} by A12;
then A26: dom (t1 . b) = F1 . b by CAT_1:5
.= cod (F1 /. f) by A4, CAT_1:5 ;
A27: Hom ((F1 . a),(G1 . a)) <> {} by A12;
then A28: (G1 /. f) * (t1 . a) = (G1 /. f) (*) (t1 . a) by A19, CAT_1:def 13;
A29: cod (t1 . a) = G1 . a by A27, CAT_1:5
.= dom (G1 /. f) by A19, CAT_1:5 ;
A30: dom (t2 . b) = F2 . b by A11, CAT_1:5
.= cod (F2 /. f) by A20, CAT_1:5 ;
A31: (t1 . b) * (F1 /. f) = (t1 . b) (*) (F1 /. f) by A25, A4, CAT_1:def 13;
A32: Hom ((<:F1,F2:> . b),(<:G1,G2:> . b)) <> {} by A16;
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 A32, CAT_1:def 13
.= [((G1 /. f) * (t1 . a)),((G2 /. f) * (t2 . a))] by A5, A13, A9, A26, A30, A31, A21, CAT_2:29
.= (<:G1,G2:> /. f) (*) (<:t1,t2:> . a) by A28, A23, A29, A24, A7, A14, CAT_2:29
.= (<:G1,G2:> /. f) * (<:t1,t2:> . a) by A17, A18, CAT_1:def 13 ;
:: thesis: verum