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