let C, A, B be non empty transitive with_units AltCatStr ; :: thesis:
let F1, F2, F3 be covariant Functor of A,B; :: thesis:
let G1 be covariant Functor of B,C; :: thesis:
let p be transformation of F1,F2; :: thesis:
let p1 be transformation of F2,F3; :: thesis:
assume A1: ( F1 is_transformable_to F2 & F2 is_transformable_to F3 ) ; :: thesis:
then F1 is_transformable_to F3 by FUNCTOR2:4;
then A2: G1 * F1 is_transformable_to G1 * F3 by Th10;
A3: ( G1 * F1 is_transformable_to G1 * F2 & G1 * F2 is_transformable_to G1 * F3 ) by A1, Th10;

now

let a be object of A; :: thesis:
A4: ( <^(F1 . a),(F2 . a)^> <> {} & <^(F2 . a),(F3 . a)^> <> {} ) by A1, FUNCTOR2:def 1;
A5: ( G1 . (F1 . a) = (G1 * F1) . a & G1 . (F2 . a) = (G1 * F2) . a & G1 . (F3 . a) = (G1 * F3) . a ) by FUNCTOR0:34;
then reconsider G1ta = (G1 * p) ! a as Morphism of (G1 . (F1 . a)),(G1 . (F2 . a)) ;
thus (G1 * (p1 `*` p)) ! a = G1 . ((p1 `*` p) ! a) by A1, Th11, FUNCTOR2:4
.= G1 . ((p1 ! a) * (p ! a)) by A1, FUNCTOR2:def 5
.= (G1 . (p1 ! a)) * (G1 . (p ! a)) by A4, FUNCTOR0:def 24
.= (G1 . (p1 ! a)) * G1ta by A1, Th11
.= ((G1 * p1) ! a) * ((G1 * p) ! a) by A1, A5, Th11
.= ((G1 * p1) `*` (G1 * p)) ! a by A3, FUNCTOR2:def 5 ; :: thesis:

end;

hence G1 * (p1 `*` p) = (G1 * p1) `*` (G1 * p) by A2, FUNCTOR2:5; :: thesis: