let A, B, C be category; :: thesis: for F1 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let F1 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C
for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let G1, G2 be covariant Functor of B,C; :: thesis: for s being natural_transformation of G1,G2 st G1 is_naturally_transformable_to G2 holds
s * F1 is natural_transformation of G1 * F1,G2 * F1
let s be natural_transformation of G1,G2; :: thesis: ( G1 is_naturally_transformable_to G2 implies s * F1 is natural_transformation of G1 * F1,G2 * F1 )
assume A1: G1 is_naturally_transformable_to G2 ; :: thesis: s * F1 is natural_transformation of G1 * F1,G2 * F1
F1 is_naturally_transformable_to F1 by FUNCTOR2:9;
hence G1 * F1 is_naturally_transformable_to G2 * F1 by A1, Lm2; :: according to FUNCTOR2:def 7 :: thesis: for b₁, b₂ being M2(the carrier of A) holds
( <^b₁,b₂^> = {} or for b₃ being M2(<^b₁,b₂^>) holds ((s * F1) ! b₂) * ((G1 * F1) . b₃) = ((G2 * F1) . b₃) * ((s * F1) ! b₁) )
let a, b be object of A; :: thesis: ( <^a,b^> = {} or for b₁ being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b₁) = ((G2 * F1) . b₁) * ((s * F1) ! a) )
assume A2: <^a,b^> <> {} ; :: thesis: for b₁ being M2(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b₁) = ((G2 * F1) . b₁) * ((s * F1) ! a)
let f be Morphism of a,b; :: thesis: ((s * F1) ! b) * ((G1 * F1) . f) = ((G2 * F1) . f) * ((s * F1) ! a)
A3: G1 is_transformable_to G2 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: (G2 * F1) . a = G2 . (F1 . a) by FUNCTOR0:34;
A7: (G2 * F1) . b = G2 . (F1 . b) by FUNCTOR0:34;
A8: (G2 * F1) . b = G2 . (F1 . b) by FUNCTOR0:34;
A9: <^(F1 . a),(F1 . b)^> <> {} by A2, FUNCTOR0:def 19;
reconsider sF1b = s ! (F1 . b) as Morphism of ((G1 * F1) . b),((G2 * F1) . b) by A7, FUNCTOR0:34;
reconsider sF1a = s ! (F1 . a) as Morphism of (G1 . (F1 . a)),((G2 * F1) . a) by FUNCTOR0:34;
reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by A4, FUNCTOR0:34;
thus ((s * F1) ! b) * ((G1 * F1) . f) = sF1b * ((G1 * F1) . f) by A3, Th12
.= sF1b * G1F1f by A2, Th6
.= (G2 . (F1 . f)) * (s ! (F1 . a)) by A1, A4, A5, A8, A9, FUNCTOR2:def 7
.= ((G2 * F1) . f) * sF1a by A2, A6, A7, Th6
.= ((G2 * F1) . f) * ((s * F1) ! a) by A3, A4, Th12 ; :: thesis: verum