let A, B, C, D be non empty transitive with_units AltCatStr ; for F1 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let F1 be covariant Functor of A,B; for G1 being covariant Functor of B,C
for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let G1 be covariant Functor of B,C; for H1, H2 being covariant Functor of C,D
for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let H1, H2 be covariant Functor of C,D; for r being transformation of H1,H2 st H1 is_transformable_to H2 holds
(r * G1) * F1 = r * (G1 * F1)
let r be transformation of H1,H2; ( H1 is_transformable_to H2 implies (r * G1) * F1 = r * (G1 * F1) )
A1:
(H2 * G1) * F1 = H2 * (G1 * F1)
by FUNCTOR0:32;
then reconsider m = r * (G1 * F1) as transformation of (H1 * G1) * F1,(H2 * G1) * F1 by FUNCTOR0:32;
assume A2:
H1 is_transformable_to H2
; (r * G1) * F1 = r * (G1 * F1)
H1 * G1 is_transformable_to H2 * G1
by A2, Th10;
hence
(r * G1) * F1 = r * (G1 * F1)
by A3, Th10, FUNCTOR2:3; verum