let A, B, C, D be Category; :: thesis: for F1, F2 being Functor of A,B
for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let F1, F2 be Functor of A,B; :: thesis: for G being Functor of B,C
for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let G be Functor of B,C; :: thesis: for H being Functor of C,D
for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let H be Functor of C,D; :: thesis: for s being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 holds
(H * G) * s = H * (G * s)
let s be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 implies (H * G) * s = H * (G * s) )
assume A1: F1 is_naturally_transformable_to F2 ; :: thesis: (H * G) * s = H * (G * s)
A2: H * (G * F1) = (H * G) * F1 by RELAT_1:36;
then reconsider v = H * (G * s) as natural_transformation of (H * G) * F1,(H * G) * F2 by RELAT_1:36;
A3: H * (G * F2) = (H * G) * F2 by RELAT_1:36;

now :: thesis: for a being Object of A holds ((H * G) * s) . a = v . a

let a be Object of A; :: thesis: ((H * G) * s) . a = v . a
A4: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:76;
A5: Hom ((F1 . a),(F2 . a)) <> {} by A1, Th23;
thus ((H * G) * s) . a = (H * G) /. (s . a) by A1, Th21
.= H /. (G /. (s . a)) by A5, NATTRA_1:11
.= H /. ((G * s) . a) by A1, A4, Th21
.= v . a by A1, A2, A3, Th20, Th21 ; :: thesis: verum

end;

hence (H * G) * s = H * (G * s) by A1, Th20, Th24; :: thesis: verum