let A, B, C, D be Category; 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; 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; 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; 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; ( G1 is_naturally_transformable_to G2 implies (H * t) * F = H * (t * F) )
assume A1:
G1 is_naturally_transformable_to G2
; (H * t) * F = H * (t * F)
A2:
H * (G1 * F) = (H * G1) * F
by RELAT_1:36;
then reconsider v = H * (t * F) as natural_transformation of (H * G1) * F,(H * G2) * F by RELAT_1:36;
A3:
H * (G2 * F) = (H * G2) * F
by RELAT_1:36;
H * G1 is_naturally_transformable_to H * G2
by A1, Th20;
hence
(H * t) * F = H * (t * F)
by A4, Th20, Th24; verum