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 ; :: according to FUNCTOR2:def 7 :: thesis: for b1, b2 being M3( the carrier of A) holds
( <^b1,b2^> = {} or for b3 being M3(<^b1,b2^>) holds ((s * F1) ! b2) * ((G1 * F1) . b3) = ((G2 * F1) . b3) * ((s * F1) ! b1) )

let a, b be Object of A; :: thesis: ( <^a,b^> = {} or for b1 being M3(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a) )
assume A2: <^a,b^> <> {} ; :: thesis: for b1 being M3(<^a,b^>) holds ((s * F1) ! b) * ((G1 * F1) . b1) = ((G2 * F1) . b1) * ((s * F1) ! a)
A3: <^(F1 . a),(F1 . b)^> <> {} by ;
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
.= (G2 . (F1 . f)) * (s ! (F1 . a)) by
.= ((G2 * F1) . f) * sF1a by A2, A4, A5, Th6
.= ((G2 * F1) . f) * ((s * F1) ! a) by A8, A7, Th12 ;
:: thesis: verum