let A, B, C 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 that
A1: F1 is_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 ; :: thesis: q (#) p = (G2 * p) `*` (q * F1)
A3: G1 * F1 is_transformable_to G1 * F2 by A1, Th10;
A4: G2 * F1 is_transformable_to G2 * F2 by A1, Th10;
A5: G1 is_transformable_to G2 by A2;
then A6: G1 * F1 is_transformable_to G2 * F1 by Th10;
A7: G1 * F2 is_transformable_to G2 * F2 by A5, Th10;

now :: thesis: for a being Object of A holds ((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! a

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

end;

hence q (#) p = (G2 * p) `*` (q * F1) by A1, A5, Th10, FUNCTOR2:3; :: thesis: verum