let A, B, C be Category; :: thesis: for F1, F2 being Functor of A,B
for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2
let F1, F2 be Functor of A,B; :: thesis: for G1, G2 being Functor of B,C st F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
G1 * F1 is_naturally_transformable_to G2 * F2
let G1, G2 be Functor of B,C; :: thesis: ( F1 is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 implies G1 * F1 is_naturally_transformable_to G2 * F2 )
assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; :: thesis: G1 * F1 is_naturally_transformable_to G2 * F2
consider t1 being natural_transformation of F1,F2, t2 being natural_transformation of G1,G2;
A3: G1 is_transformable_to G2 by A2, NATTRA_1:def 7;
A4: F1 is_transformable_to F2 by A1, NATTRA_1:def 7;
hence A5: G1 * F1 is_transformable_to G2 * F2 by A3, Th8; :: according to NATTRA_1:def 7 :: thesis: ex b₁ being transformation of G1 * F1,G2 * F2 st
for b₂, b₃ being M2(the carrier of A) holds
( Hom b₂,b₃ = {} or for b₄ being Morphism of b₂,b₃ holds (b₁ . b₃) * ((G1 * F1) . b₄) = ((G2 * F2) . b₄) * (b₁ . b₂) )
take t = (t2 * F2) `*` (G1 * t1); :: thesis: for b₁, b₂ being M2(the carrier of A) holds
( Hom b₁,b₂ = {} or for b₃ being Morphism of b₁,b₂ holds (t . b₂) * ((G1 * F1) . b₃) = ((G2 * F2) . b₃) * (t . b₁) )
let a, b be Object of A; :: thesis: ( Hom a,b = {} or for b₁ being Morphism of a,b holds (t . b) * ((G1 * F1) . b₁) = ((G2 * F2) . b₁) * (t . a) )
A6: Hom (G1 . (F2 . b)),(G2 . (F2 . b)) <> {} by A3, NATTRA_1:def 2;
A7: Hom ((G1 * F1) . a),((G2 * F2) . a) <> {} by A5, NATTRA_1:def 2;
A8: G1 * F1 is_transformable_to G1 * F2 by A4, Th8;
then A9: Hom ((G1 * F1) . b),((G1 * F2) . b) <> {} by NATTRA_1:def 2;
A10: Hom ((G1 * F1) . b),((G2 * F2) . b) <> {} by A5, NATTRA_1:def 2;
assume A11: Hom a,b <> {} ; :: thesis: for b₁ being Morphism of a,b holds (t . b) * ((G1 * F1) . b₁) = ((G2 * F2) . b₁) * (t . a)
then A12: Hom ((G2 * F2) . a),((G2 * F2) . b) <> {} by CAT_1:126;
A13: Hom (F1 . b),(F2 . b) <> {} by A4, NATTRA_1:def 2;
then A14: Hom (G1 . (F1 . b)),(G1 . (F2 . b)) <> {} by CAT_1:126;
then A15: Hom (G1 . (F1 . b)),(G2 . (F2 . b)) <> {} by A6, CAT_1:52;
A16: G1 * F2 is_transformable_to G2 * F2 by A3, Th8;
then A17: Hom ((G1 * F2) . b),((G2 * F2) . b) <> {} by NATTRA_1:def 2;
A18: Hom ((G1 * F1) . a),((G1 * F2) . a) <> {} by A8, NATTRA_1:def 2;
A19: Hom ((G1 * F2) . a),((G2 * F2) . a) <> {} by A16, NATTRA_1:def 2;
A20: Hom (F1 . a),(F2 . a) <> {} by A4, NATTRA_1:def 2;
then A21: Hom (G1 . (F1 . a)),(G1 . (F2 . a)) <> {} by CAT_1:126;
let f be Morphism of a,b; :: thesis: (t . b) * ((G1 * F1) . f) = ((G2 * F2) . f) * (t . a)
A22: Hom (F2 . a),(F2 . b) <> {} by A11, CAT_1:126;
then A23: Hom (G1 . (F2 . a)),(G1 . (F2 . b)) <> {} by CAT_1:126;
A24: Hom (F1 . a),(F1 . b) <> {} by A11, CAT_1:126;
then A25: Hom (G1 . (F1 . a)),(G1 . (F1 . b)) <> {} by CAT_1:126;
A26: Hom (G1 . (F2 . a)),(G2 . (F2 . a)) <> {} by A3, NATTRA_1:def 2;
then A27: Hom (G1 . (F1 . a)),(G2 . (F2 . a)) <> {} by A21, CAT_1:52;
A28: Hom (G2 . (F2 . a)),(G2 . (F2 . b)) <> {} by A22, CAT_1:126;
Hom ((G1 * F1) . a),((G1 * F1) . b) <> {} by A11, CAT_1:126;
hence (t . b) * ((G1 * F1) . f) = (t . b) * ((G1 * F1) . f) by A10, CAT_1:def 13
.= (t . b) * (G1 . (F1 . f)) by A11, NATTRA_1:11
.= (((t2 * F2) . b) * ((G1 * t1) . b)) * (G1 . (F1 . f)) by A8, A16, NATTRA_1:def 6
.= (((t2 * F2) . b) * ((G1 * t1) . b)) * (G1 . (F1 . f)) by A17, A9, CAT_1:def 13
.= (((t2 * F2) . b) * (G1 . (t1 . b))) * (G1 . (F1 . f)) by A4, Th26
.= ((t2 . (F2 . b)) * (G1 . (t1 . b))) * (G1 . (F1 . f)) by A3, Th25
.= ((t2 . (F2 . b)) * (G1 . (t1 . b))) * (G1 . (F1 . f)) by A6, A14, CAT_1:def 13
.= ((t2 . (F2 . b)) * (G1 . (t1 . b))) * (G1 . (F1 . f)) by A25, A15, CAT_1:def 13
.= (t2 . (F2 . b)) * ((G1 . (t1 . b)) * (G1 . (F1 . f))) by A6, A14, A25, CAT_1:54
.= (t2 . (F2 . b)) * (G1 . ((t1 . b) * (F1 . f))) by A13, A24, NATTRA_1:13
.= (t2 . (F2 . b)) * (G1 . ((F2 . f) * (t1 . a))) by A1, A11, NATTRA_1:def 8
.= (t2 . (F2 . b)) * ((G1 . (F2 . f)) * (G1 . (t1 . a))) by A22, A20, NATTRA_1:13
.= ((t2 . (F2 . b)) * (G1 . (F2 . f))) * (G1 . (t1 . a)) by A6, A23, A21, CAT_1:54
.= ((G2 . (F2 . f)) * (t2 . (F2 . a))) * (G1 . (t1 . a)) by A2, A22, NATTRA_1:def 8
.= (G2 . (F2 . f)) * ((t2 . (F2 . a)) * (G1 . (t1 . a))) by A21, A28, A26, CAT_1:54
.= (G2 . (F2 . f)) * ((t2 . (F2 . a)) * (G1 . (t1 . a))) by A28, A27, CAT_1:def 13
.= (G2 . (F2 . f)) * ((t2 . (F2 . a)) * (G1 . (t1 . a))) by A21, A26, CAT_1:def 13
.= (G2 . (F2 . f)) * (((t2 * F2) . a) * (G1 . (t1 . a))) by A3, Th25
.= (G2 . (F2 . f)) * (((t2 * F2) . a) * ((G1 * t1) . a)) by A4, Th26
.= (G2 . (F2 . f)) * (((t2 * F2) . a) * ((G1 * t1) . a)) by A19, A18, CAT_1:def 13
.= (G2 . (F2 . f)) * (t . a) by A8, A16, NATTRA_1:def 6
.= ((G2 * F2) . f) * (t . a) by A11, NATTRA_1:11
.= ((G2 * F2) . f) * (t . a) by A7, A12, CAT_1:def 13 ;
:: thesis: verum