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

now

let a be Object of A; :: thesis: ((H * t) * F) . a = v . a
A4: ( G1 . (F . a) = (G1 * F) . a & G2 . (F . a) = (G2 * F) . a ) by CAT_1:113;
thus ((H * t) * F) . a = (H * t) . (F . a) by A1, Th27, Th29
.= H . (t . (F . a)) by A1, Th28
.= H . ((t * F) . a) by A1, A4, Th29
.= v . a by A1, A3, Th27, Th28 ; :: thesis: verum

end;

hence (H * t) * F = H * (t * F) by A2, Th31; :: thesis: verum