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
set t1 = the natural_transformation of F1,F2;
set t2 = the natural_transformation of G1,G2;
A3: G1 is_transformable_to G2 by A2;
A4: F1 is_transformable_to F2 by A1;
hence A5: G1 * F1 is_transformable_to G2 * F2 by A3, Th3; :: according to NATTRA_1:def 7 :: thesis: ex b₁ being transformation of G1 * F1,G2 * F2 st
for b₂, b₃ being M3( 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 = ( the natural_transformation of G1,G2 * F2) `*` (G1 * the natural_transformation of F1,F2); :: thesis: for b₁, b₂ being M3( 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;
A7: Hom (((G1 * F1) . a),((G2 * F2) . a)) <> {} by A5;
A8: G1 * F1 is_transformable_to G1 * F2 by A4, Th3;
then A9: Hom (((G1 * F1) . b),((G1 * F2) . b)) <> {} ;
A10: Hom (((G1 * F1) . b),((G2 * F2) . b)) <> {} by A5;
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:84;
A13: Hom ((F1 . b),(F2 . b)) <> {} by A4;
then A14: Hom ((G1 . (F1 . b)),(G1 . (F2 . b))) <> {} by CAT_1:84;
then A15: Hom ((G1 . (F1 . b)),(G2 . (F2 . b))) <> {} by A6, CAT_1:24;
A16: G1 * F2 is_transformable_to G2 * F2 by A3, Th3;
then A17: Hom (((G1 * F2) . b),((G2 * F2) . b)) <> {} ;
A18: Hom (((G1 * F1) . a),((G1 * F2) . a)) <> {} by A8;
A19: Hom (((G1 * F2) . a),((G2 * F2) . a)) <> {} by A16;
A20: Hom ((F1 . a),(F2 . a)) <> {} by A4;
then A21: Hom ((G1 . (F1 . a)),(G1 . (F2 . a))) <> {} by CAT_1:84;
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:84;
then A23: Hom ((G1 . (F2 . a)),(G1 . (F2 . b))) <> {} by CAT_1:84;
A24: Hom ((F1 . a),(F1 . b)) <> {} by A11, CAT_1:84;
then A25: Hom ((G1 . (F1 . a)),(G1 . (F1 . b))) <> {} by CAT_1:84;
A26: Hom ((G1 . (F2 . a)),(G2 . (F2 . a))) <> {} by A3;
then A27: Hom ((G1 . (F1 . a)),(G2 . (F2 . a))) <> {} by A21, CAT_1:24;
A28: Hom ((G2 . (F2 . a)),(G2 . (F2 . b))) <> {} by A22, CAT_1:84;
Hom (((G1 * F1) . a),((G1 * F1) . b)) <> {} by A11, CAT_1:84;
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
.= ((( the natural_transformation of G1,G2 * F2) . b) * ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A8, A16, NATTRA_1:def 6
.= ((( the natural_transformation of G1,G2 * F2) . b) (*) ((G1 * the natural_transformation of F1,F2) . b)) (*) (G1 /. (F1 /. f)) by A17, A9, CAT_1:def 13
.= ((( the natural_transformation of G1,G2 * F2) . b) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A4, Th19
.= (( the natural_transformation of G1,G2 . (F2 . b)) (*) (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A3, Th18
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) (*) (G1 /. (F1 /. f)) by A6, A14, CAT_1:def 13
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ( the natural_transformation of F1,F2 . b))) * (G1 /. (F1 /. f)) by A25, A15, CAT_1:def 13
.= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. ( the natural_transformation of F1,F2 . b)) * (G1 /. (F1 /. f))) by A6, A14, A25, CAT_1:25
.= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (( the natural_transformation of F1,F2 . b) * (F1 /. f))) by A13, A24, NATTRA_1:13
.= ( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. ((F2 /. f) * ( the natural_transformation of F1,F2 . a))) by A1, A11, NATTRA_1:def 8
.= ( the natural_transformation of G1,G2 . (F2 . b)) * ((G1 /. (F2 /. f)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A22, A20, NATTRA_1:13
.= (( the natural_transformation of G1,G2 . (F2 . b)) * (G1 /. (F2 /. f))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A6, A23, A21, CAT_1:25
.= ((G2 /. (F2 /. f)) * ( the natural_transformation of G1,G2 . (F2 . a))) * (G1 /. ( the natural_transformation of F1,F2 . a)) by A2, A22, NATTRA_1:def 8
.= (G2 /. (F2 /. f)) * (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A28, A26, CAT_1:25
.= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) * (G1 /. ( the natural_transformation of F1,F2 . a))) by A28, A27, CAT_1:def 13
.= (G2 /. (F2 /. f)) (*) (( the natural_transformation of G1,G2 . (F2 . a)) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A21, A26, CAT_1:def 13
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) (G1 /. ( the natural_transformation of F1,F2 . a))) by A3, Th18
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) (*) ((G1 * the natural_transformation of F1,F2) . a)) by A4, Th19
.= (G2 /. (F2 /. f)) (*) ((( the natural_transformation of G1,G2 * F2) . a) * ((G1 * the natural_transformation of F1,F2) . 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