let C, A, B be category; :: thesis: for F1, F2 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let F1, F2 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C
for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let G1 be covariant Functor of B,C; :: thesis: for t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
G1 * t is natural_transformation of G1 * F1,G1 * F2
let t be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies G1 * t is natural_transformation of G1 * F1,G1 * F2 )
assume A1:
F1 is_naturally_transformable_to F2
; :: thesis: G1 * t is natural_transformation of G1 * F1,G1 * F2
G1 is_naturally_transformable_to G1
by FUNCTOR2:9;
hence
G1 * F1 is_naturally_transformable_to G1 * F2
by A1, Lm2; :: according to FUNCTOR2:def 7 :: thesis: for b1, b2 being M2(the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M2(<^b1,b2^>) holds ((G1 * t) ! b2) * ((G1 * F1) . b3) = ((G1 * F2) . b3) * ((G1 * t) ! b1) )
let a, b be object of A; :: thesis: ( <^a,b^> = {} or for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a) )
assume A2:
<^a,b^> <> {}
; :: thesis: for b1 being M2(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a)
let f be Morphism of a,b; :: thesis: ((G1 * t) ! b) * ((G1 * F1) . f) = ((G1 * F2) . f) * ((G1 * t) ! a)
A3:
F1 is_transformable_to F2
by A1, FUNCTOR2:def 6;
A4:
(G1 * F1) . a = G1 . (F1 . a)
by FUNCTOR0:34;
A5:
(G1 * F1) . b = G1 . (F1 . b)
by FUNCTOR0:34;
A6:
(G1 * F2) . a = G1 . (F2 . a)
by FUNCTOR0:34;
A7:
(G1 * F2) . b = G1 . (F2 . b)
by FUNCTOR0:34;
A8:
<^(F1 . a),(F1 . b)^> <> {}
by A2, FUNCTOR0:def 19;
A9:
<^(F1 . a),(F2 . a)^> <> {}
by A3, FUNCTOR2:def 1;
A10:
<^(F1 . b),(F2 . b)^> <> {}
by A3, FUNCTOR2:def 1;
A11:
<^(F2 . a),(F2 . b)^> <> {}
by A2, FUNCTOR0:def 19;
reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),(G1 . (F2 . b)) by FUNCTOR0:34;
reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A4, FUNCTOR0:34;
reconsider G1ta = G1 . (t ! a) as Morphism of (G1 . (F1 . a)),((G1 * F2) . a) by FUNCTOR0:34;
thus ((G1 * t) ! b) * ((G1 * F1) . f) =
G1tb * ((G1 * F1) . f)
by A3, A7, Th11
.=
G1tb * G1F1f
by A2, Th6
.=
G1 . ((t ! b) * (F1 . f))
by A4, A5, A8, A10, FUNCTOR0:def 24
.=
G1 . ((F2 . f) * (t ! a))
by A1, A2, FUNCTOR2:def 7
.=
(G1 . (F2 . f)) * (G1 . (t ! a))
by A9, A11, FUNCTOR0:def 24
.=
((G1 * F2) . f) * G1ta
by A2, A6, A7, Th6
.=
((G1 * F2) . f) * ((G1 * t) ! a)
by A3, A4, Th11
; :: thesis: verum