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 A1, A2, Th12, FUNCTOR2:2
.= (q1 ! (F1 . a)) * (q ! (F1 . a)) by A1, A2, FUNCTOR2:def 5
.= s1F1a * (q ! (F1 . a)) by A2, Th12
.= ((q1 * F1) ! a) * ((q * F1) ! a) by A1, A6, A5, Th12
.= ((q1 * F1) `*` (q * F1)) ! a by A3, FUNCTOR2:def 5 ; :: thesis: verum

end;

G1 is_transformable_to G3 by A1, A2, FUNCTOR2:2;
hence (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) by A4, Th10, FUNCTOR2:3; :: thesis: verum