let C, A, B be non empty transitive with_units AltCatStr ; :: thesis: for F1, F2 being covariant Functor of A,B
for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let F1, F2 be covariant Functor of A,B; :: thesis: for G1, G2 being covariant Functor of B,C
for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let G1, G2 be covariant Functor of B,C; :: thesis: for p being transformation of F1,F2
for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let p be transformation of F1,F2; :: thesis: for q being natural_transformation of G1,G2 st F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 holds
q (#) p = (G2 * p) `*` (q * F1)
let q be natural_transformation of G1,G2; :: thesis: ( F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 implies q (#) p = (G2 * p) `*` (q * F1) )
assume A1: ( F1 is_transformable_to F2 & G1 is_naturally_transformable_to G2 ) ; :: thesis: q (#) p = (G2 * p) `*` (q * F1)
then A2: G1 is_transformable_to G2 by FUNCTOR2:def 6;
then A3: G1 * F1 is_transformable_to G2 * F2 by A1, Th10;
A4: ( G1 * F2 is_transformable_to G2 * F2 & G1 * F1 is_transformable_to G1 * F2 ) by A1, A2, Th10;
A5: ( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G2 * F2 ) by A1, A2, Th10;

now

let a be object of A; :: thesis: ((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! a
A6: ( G1 . (F1 . a) = (G1 * F1) . a & G1 . (F2 . a) = (G1 * F2) . a & G2 . (F1 . a) = (G2 * F1) . a & G2 . (F2 . a) = (G2 * F2) . a ) by FUNCTOR0:34;
then reconsider sF2a = q ! (F2 . a) as Morphism of ((G1 * F2) . a),((G2 * F2) . a) ;
reconsider G2ta = (G2 * p) ! a as Morphism of (G2 . (F1 . a)),(G2 . (F2 . a)) by A6;
A7: <^(F1 . a),(F2 . a)^> <> {} by A1, FUNCTOR2:def 1;
thus ((q * F2) `*` (G1 * p)) ! a = ((q * F2) ! a) * ((G1 * p) ! a) by A4, FUNCTOR2:def 5
.= sF2a * ((G1 * p) ! a) by A2, Th12
.= (q ! (F2 . a)) * (G1 . (p ! a)) by A1, A6, Th11
.= (G2 . (p ! a)) * (q ! (F1 . a)) by A1, A7, FUNCTOR2:def 7
.= G2ta * (q ! (F1 . a)) by A1, Th11
.= ((G2 * p) ! a) * ((q * F1) ! a) by A2, A6, Th12
.= ((G2 * p) `*` (q * F1)) ! a by A5, FUNCTOR2:def 5 ; :: thesis: verum

end;

hence q (#) p = (G2 * p) `*` (q * F1) by A3, FUNCTOR2:5; :: thesis: verum