let A, B, C be non empty transitive with_units AltCatStr ; :: thesis: for F1 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let F1 be covariant Functor of A,B; :: thesis: for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let G1, G2, G3 be covariant Functor of B,C; :: thesis: for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q be transformation of G1,G2; :: thesis: for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q1 be transformation of G2,G3; :: thesis: ( G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) )
assume A1: ( G1 is_transformable_to G2 & G2 is_transformable_to G3 ) ; :: thesis: (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
then G1 is_transformable_to G3 by FUNCTOR2:4;
then A2: G1 * F1 is_transformable_to G3 * F1 by Th10;
A3: ( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 ) by A1, Th10;

now

let a be object of A; :: thesis: ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! a
A4: ( G1 . (F1 . a) = (G1 * F1) . a & G2 . (F1 . a) = (G2 * F1) . a & G3 . (F1 . a) = (G3 * F1) . a ) by FUNCTOR0:34;
then reconsider s1F1a = (q1 * F1) ! a as Morphism of (G2 . (F1 . a)),(G3 . (F1 . a)) ;
thus ((q1 `*` q) * F1) ! a = (q1 `*` q) ! (F1 . a) by A1, Th12, FUNCTOR2:4
.= (q1 ! (F1 . a)) * (q ! (F1 . a)) by A1, FUNCTOR2:def 5
.= s1F1a * (q ! (F1 . a)) by A1, Th12
.= ((q1 * F1) ! a) * ((q * F1) ! a) by A1, A4, Th12
.= ((q1 * F1) `*` (q * F1)) ! a by A3, FUNCTOR2:def 5 ; :: thesis: verum

end;

hence (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) by A2, FUNCTOR2:5; :: thesis: verum