let A, B, C, D be Category; 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; 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; 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; 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; ( H1 is_naturally_transformable_to H2 implies (u * G) * F = u * (G * F) )
assume A1:
H1 is_naturally_transformable_to H2
; (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;
H1 * G is_naturally_transformable_to H2 * G
by A1, Th20;
hence
(u * G) * F = u * (G * F)
by A4, Th20, Th24; verum