let A, B, C 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
then A2: F1 is_transformable_to F2 ;
thus G1 * F1 is_naturally_transformable_to G1 * F2 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 ((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 M3(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a) )
assume A3: <^a,b^> <> {} ; :: thesis: for b1 being M3(<^a,b^>) holds ((G1 * t) ! b) * ((G1 * F1) . b1) = ((G1 * F2) . b1) * ((G1 * t) ! a)
A4: ( (G1 * F1) . b = G1 . (F1 . b) & <^(F1 . a),(F1 . b)^> <> {} ) by ;
A5: <^(F1 . b),(F2 . b)^> <> {} by A2;
A6: <^(F1 . a),(F2 . a)^> <> {} by A2;
reconsider G1ta = G1 . (t ! a) as Morphism of (G1 . (F1 . a)),((G1 * F2) . a) by FUNCTOR0:33;
reconsider G1tb = G1 . (t ! b) as Morphism of ((G1 * F1) . b),(G1 . (F2 . b)) by FUNCTOR0:33;
let f be Morphism of a,b; :: thesis: ((G1 * t) ! b) * ((G1 * F1) . f) = ((G1 * F2) . f) * ((G1 * t) ! a)
A7: (G1 * F2) . a = G1 . (F2 . a) by FUNCTOR0:33;
A8: <^(F2 . a),(F2 . b)^> <> {} by ;
A9: (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;
A10: (G1 * F2) . b = G1 . (F2 . b) by FUNCTOR0:33;
hence ((G1 * t) ! b) * ((G1 * F1) . f) = G1tb * ((G1 * F1) . f) by
.= G1tb * G1F1f by
.= G1 . ((t ! b) * (F1 . f)) by
.= G1 . ((F2 . f) * (t ! a)) by
.= (G1 . (F2 . f)) * (G1 . (t ! a)) by
.= ((G1 * F2) . f) * G1ta by A3, A7, A10, Th6
.= ((G1 * F2) . f) * ((G1 * t) ! a) by A2, A9, Th11 ;
:: thesis: verum