let C, D, A, B 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)
then A2: ( G * F1 is_naturally_transformable_to G * F2 & (H * G) * F1 is_naturally_transformable_to (H * G) * F2 ) by Th27;
A3: ( H * (G * F1) = (H * G) * F1 & H * (G * F2) = (H * G) * F2 ) by RELAT_1:55;
then reconsider v = H * (G * s) as natural_transformation of (H * G) * F1,(H * G) * F2 ;

now

let a be Object of A; :: thesis: ((H * G) * s) . a = v . a
A4: Hom (F1 . a),(F2 . a) <> {} by A1, Th30;
A5: ( G . (F1 . a) = (G * F1) . a & G . (F2 . a) = (G * F2) . a ) by CAT_1:113;
thus ((H * G) * s) . a = (H * G) . (s . a) by A1, Th28
.= H . (G . (s . a)) by A4, NATTRA_1:11
.= H . ((G * s) . a) by A1, A5, Th28
.= v . a by A1, A3, Th27, Th28 ; :: thesis: verum

end;

hence (H * G) * s = H * (G * s) by A2, Th31; :: thesis: verum