let A, B, C be non empty transitive with_units AltCatStr ; 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; 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; 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; 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; ( 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
; 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 for a being Object of A holds ((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! alet a be
Object of
A;
((q * F2) `*` (G1 * p)) ! a = ((G2 * p) `*` (q * F1)) ! aA8:
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
;
verum end;
hence
q (#) p = (G2 * p) `*` (q * F1)
by A1, A5, Th10, FUNCTOR2:3; verum