let A, B, C be Category; 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; 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; 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; 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; ( 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 )
; (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;
hence
(t9 `*` t) * F = (t9 * F) `*` (t * F)
by A2, Th24, NATTRA_1:23; verum