let A, B, C be Category; 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; 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; ( 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
; 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; NATTRA_1:def 7 ex b1 being transformation of G1 * F1,G2 * F2 st
for b2, b3 being M3( the carrier of A) holds
( Hom (b2,b3) = {} or for b4 being Morphism of b2,b3 holds (b1 . b3) * ((G1 * F1) /. b4) = ((G2 * F2) /. b4) * (b1 . b2) )
take t = ( the natural_transformation of G1,G2 * F2) `*` (G1 * the natural_transformation of F1,F2); for b1, b2 being M3( the carrier of A) holds
( Hom (b1,b2) = {} or for b3 being Morphism of b1,b2 holds (t . b2) * ((G1 * F1) /. b3) = ((G2 * F2) /. b3) * (t . b1) )
let a, b be Object of A; ( Hom (a,b) = {} or for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (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) <> {}
; for b1 being Morphism of a,b holds (t . b) * ((G1 * F1) /. b1) = ((G2 * F2) /. b1) * (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; (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
;
verum