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 that
A1: G1 is_transformable_to G2 and
A2: G2 is_transformable_to G3 ; :: thesis: (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
A3: ( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 ) by A1, A2, Th10;
A4: now :: thesis: for a being Object of A holds ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! a
let a be Object of A; :: thesis: ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! a
A5: ( G1 . (F1 . a) = (G1 * F1) . a & G3 . (F1 . a) = (G3 * F1) . a ) by FUNCTOR0:33;
A6: G2 . (F1 . a) = (G2 * F1) . a by FUNCTOR0:33;
then reconsider s1F1a = (q1 * F1) ! a as Morphism of (G2 . (F1 . a)),(G3 . (F1 . a)) by FUNCTOR0:33;
thus ((q1 `*` q) * F1) ! a = (q1 `*` q) ! (F1 . a) by
.= (q1 ! (F1 . a)) * (q ! (F1 . a)) by
.= s1F1a * (q ! (F1 . a)) by
.= ((q1 * F1) ! a) * ((q * F1) ! a) by A1, A6, A5, Th12
.= ((q1 * F1) `*` (q * F1)) ! a by ; :: thesis: verum
end;
G1 is_transformable_to G3 by ;
hence (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) by ; :: thesis: verum