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)
A2: H1 * (G * F) = (H1 * G) * F by RELAT_1:36;
then reconsider v = u * (G * F) as natural_transformation of (H1 * G) * F,(H2 * G) * F by RELAT_1:36;
A3: H2 * (G * F) = (H2 * G) * F by RELAT_1:36;

A4: now :: thesis: for a being Object of A holds ((u * G) * F) . a = v . a

let a be Object of A; :: thesis: ((u * G) * F) . a = v . a
thus ((u * G) * F) . a = (u * G) . (F . a) by A1, Th20, Th22
.= u . (G . (F . a)) by A1, Th22
.= u . ((G * F) . a) by CAT_1:76
.= v . a by A1, A2, A3, Th22 ; :: thesis: verum

end;

H1 * G is_naturally_transformable_to H2 * G by A1, Th20;
hence (u * G) * F = u * (G * F) by A4, Th20, Th24; :: thesis: verum