let A, B, C, D be non empty transitive with_units AltCatStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( H1 is_transformable_to H2 implies (r * G1) * F1 = r * (G1 * F1) )
assume A1: H1 is_transformable_to H2 ; :: thesis: (r * G1) * F1 = r * (G1 * F1)
A2: (H2 * G1) * F1 = H2 * (G1 * F1) by FUNCTOR0:33;
then reconsider m = r * (G1 * F1) as transformation of (H1 * G1) * F1,(H2 * G1) * F1 by FUNCTOR0:33;
H1 * G1 is_transformable_to H2 * G1 by A1, Th10;
then A3: (H1 * G1) * F1 is_transformable_to (H2 * G1) * F1 by Th10;

now

let a be object of A; :: thesis: ((r * G1) * F1) ! a = m ! a
thus ((r * G1) * F1) ! a = (r * G1) ! (F1 . a) by A1, Th10, Th12
.= r ! (G1 . (F1 . a)) by A1, Th12
.= r ! ((G1 * F1) . a) by FUNCTOR0:34
.= (r * (G1 * F1)) ! a by A1, Th12
.= m ! a by A2, FUNCTOR0:33 ; :: thesis: verum

end;

hence (r * G1) * F1 = r * (G1 * F1) by A3, FUNCTOR2:5; :: thesis: verum