let A, B, C, D be Category; :: thesis: for F being Functor of A,B
for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let F be Functor of A,B; :: thesis: for G being Functor of B,C
for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let G be Functor of B,C; :: thesis: for H1, H2 being Functor of C,D
for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let H1, H2 be Functor of C,D; :: thesis: for u being natural_transformation of H1,H2 st H1 is_naturally_transformable_to H2 holds
(u * G) * F = u * (G * F)
let u be natural_transformation of H1,H2; :: thesis: ( H1 is_naturally_transformable_to H2 implies (u * G) * F = u * (G * F) )
assume A1: H1 is_naturally_transformable_to H2 ; :: thesis: (u * G) * F = u * (G * F)
then H1 * G is_naturally_transformable_to H2 * G by Th27;
then A2: (H1 * G) * F is_naturally_transformable_to (H2 * G) * F by Th27;
A3: ( H1 * (G * F) = (H1 * G) * F & H2 * (G * F) = (H2 * G) * F ) by RELAT_1:55;
then reconsider v = u * (G * F) as natural_transformation of (H1 * G) * F,(H2 * G) * F ;

now

let a be Object of A; :: thesis: ((u * G) * F) . a = v . a
thus ((u * G) * F) . a = (u * G) . (F . a) by A1, Th27, Th29
.= u . (G . (F . a)) by A1, Th29
.= u . ((G * F) . a) by CAT_1:113
.= v . a by A1, A3, Th29 ; :: thesis: verum

end;

hence (u * G) * F = u * (G * F) by A2, Th31; :: thesis: verum