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
thus G1 * F1 is_naturally_transformable_to G2 * F1 by A1, Lm2; :: according to FUNCTOR2:def 7 :: thesis: for b₁, b₂ being M3( the carrier of A) holds
( <^b₁,b₂^> = {} or for b₃ being M3(<^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 M3(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b₁) = ((G2 * F1) . b₁) * ((s * F1) ! a) )
assume A2: <^a,b^> <> {} ; :: thesis: for b₁ being M3(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b₁) = ((G2 * F1) . b₁) * ((s * F1) ! a)
A3: <^(F1 . a),(F1 . b)^> <> {} by A2, FUNCTOR0:def 18;
reconsider sF1a = s ! (F1 . a) as Morphism of (G1 . (F1 . a)),((G2 * F1) . a) by FUNCTOR0:33;
let f be Morphism of a,b; :: thesis: ((s * F1) ! b) * ((G1 * F1) . f) = ((G2 * F1) . f) * ((s * F1) ! a)
A4: (G2 * F1) . a = G2 . (F1 . a) by FUNCTOR0:33;
A5: (G2 * F1) . b = G2 . (F1 . b) by FUNCTOR0:33;
then reconsider sF1b = s ! (F1 . b) as Morphism of ((G1 * F1) . b),((G2 * F1) . b) by FUNCTOR0:33;
A6: ( (G1 * F1) . b = G1 . (F1 . b) & (G2 * F1) . b = G2 . (F1 . b) ) by FUNCTOR0:33;
A7: (G1 * F1) . a = G1 . (F1 . a) by FUNCTOR0:33;
then reconsider G1F1f = G1 . (F1 . f) as Morphism of ((G1 * F1) . a),((G1 * F1) . b) by FUNCTOR0:33;
A8: G1 is_transformable_to G2 by A1;
hence ((s * F1) ! b) * ((G1 * F1) . f) = sF1b * ((G1 * F1) . f) by Th12
.= sF1b * G1F1f by A2, Th6
.= (G2 . (F1 . f)) * (s ! (F1 . a)) by A1, A7, A6, A3, FUNCTOR2:def 7
.= ((G2 * F1) . f) * sF1a by A2, A4, A5, Th6
.= ((G2 * F1) . f) * ((s * F1) ! a) by A8, A7, Th12 ;
:: thesis: verum