let A, B, C be Category; :: thesis: for F being Functor of A,B
for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let F be Functor of A,B; :: thesis: for G1, G2, G3 being Functor of B,C
for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let G1, G2, G3 be Functor of B,C; :: thesis: for t being natural_transformation of G1,G2
for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let t be natural_transformation of G1,G2; :: thesis: for t9 being natural_transformation of G2,G3 st G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 holds
(t9 `*` t) * F = (t9 * F) `*` (t * F)
let t9 be natural_transformation of G2,G3; :: thesis: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 implies (t9 `*` t) * F = (t9 * F) `*` (t * F) )
assume A1: ( G1 is_naturally_transformable_to G2 & G2 is_naturally_transformable_to G3 ) ; :: thesis: (t9 `*` t) * F = (t9 * F) `*` (t * F)
then A2: ( G1 * F is_naturally_transformable_to G2 * F & G2 * F is_naturally_transformable_to G3 * F ) by Th20;

now :: thesis: for a being Object of A holds ((t9 `*` t) * F) . a = ((t9 * F) `*` (t * F)) . a

let a be Object of A; :: thesis: ((t9 `*` t) * F) . a = ((t9 * F) `*` (t * F)) . a
A3: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:76;
A4: G3 . (F . a) = (G3 * F) . a by CAT_1:76;
A5: ( t9 . (F . a) = (t9 * F) . a & t . (F . a) = (t * F) . a ) by A1, Th22;
thus ((t9 `*` t) * F) . a = (t9 `*` t) . (F . a) by A1, Th22, NATTRA_1:23
.= (t9 . (F . a)) * (t . (F . a)) by A1, NATTRA_1:25
.= ((t9 * F) `*` (t * F)) . a by A2, A5, A3, A4, NATTRA_1:25 ; :: thesis: verum

end;

hence (t9 `*` t) * F = (t9 * F) `*` (t * F) by A2, Th24, NATTRA_1:23; :: thesis: verum