let A, B, C be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2, F3 being covariant Functor of A,B
for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let F1, F2, F3 be covariant Functor of A,B; :: thesis: for G1 being covariant Functor of B,C
for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let G1 be covariant Functor of B,C; :: thesis: for p being transformation of F1,F2
for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let p be transformation of F1,F2; :: thesis: for p1 being transformation of F2,F3 st F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
let p1 be transformation of F2,F3; :: thesis: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 implies G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) )
assume that
A1: F1 is_transformable_to F2 and
A2: F2 is_transformable_to F3 ; :: thesis: G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p)
A3: ( G1 * F1 is_transformable_to G1 * F2 & G1 * F2 is_transformable_to G1 * F3 ) by A1, A2, Th10;

A4: now :: thesis: for a being Object of A holds (G1 * (p1 `*` p)) ! a = ((G1 * p1) `*` (G1 * p)) ! a

let a be Object of A; :: thesis: (G1 * (p1 `*` p)) ! a = ((G1 * p1) `*` (G1 * p)) ! a
A5: ( G1 . (F2 . a) = (G1 * F2) . a & G1 . (F3 . a) = (G1 * F3) . a ) by FUNCTOR0:33;
A6: G1 . (F1 . a) = (G1 * F1) . a by FUNCTOR0:33;
then reconsider G1ta = (G1 * p) ! a as Morphism of (G1 . (F1 . a)),(G1 . (F2 . a)) by FUNCTOR0:33;
A7: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A1, A2;
thus (G1 * (p1 `*` p)) ! a = G1 . ((p1 `*` p) ! a) by A1, A2, Th11, FUNCTOR2:2
.= G1 . ((p1 ! a) * (p ! a)) by A1, A2, FUNCTOR2:def 5
.= (G1 . (p1 ! a)) * (G1 . (p ! a)) by A7, FUNCTOR0:def 23
.= (G1 . (p1 ! a)) * G1ta by A1, Th11
.= ((G1 * p1) ! a) * ((G1 * p) ! a) by A2, A6, A5, Th11
.= ((G1 * p1) `*` (G1 * p)) ! a by A3, FUNCTOR2:def 5 ; :: thesis: verum

end;

F1 is_transformable_to F3 by A1, A2, FUNCTOR2:2;
hence G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) by A4, Th10, FUNCTOR2:3; :: thesis: verum