let A, B, C be non empty transitive with_units AltCatStr ; for F1 being covariant Functor of A,B
for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let F1 be covariant Functor of A,B; for G1, G2, G3 being covariant Functor of B,C
for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let G1, G2, G3 be covariant Functor of B,C; for q being transformation of G1,G2
for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q be transformation of G1,G2; for q1 being transformation of G2,G3 st G1 is_transformable_to G2 & G2 is_transformable_to G3 holds
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
let q1 be transformation of G2,G3; ( G1 is_transformable_to G2 & G2 is_transformable_to G3 implies (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1) )
assume that
A1:
G1 is_transformable_to G2
and
A2:
G2 is_transformable_to G3
; (q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
A3:
( G1 * F1 is_transformable_to G2 * F1 & G2 * F1 is_transformable_to G3 * F1 )
by A1, A2, Th10;
A4:
now for a being Object of A holds ((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! alet a be
Object of
A;
((q1 `*` q) * F1) ! a = ((q1 * F1) `*` (q * F1)) ! aA5:
(
G1 . (F1 . a) = (G1 * F1) . a &
G3 . (F1 . a) = (G3 * F1) . a )
by FUNCTOR0:33;
A6:
G2 . (F1 . a) = (G2 * F1) . a
by FUNCTOR0:33;
then reconsider s1F1a =
(q1 * F1) ! a as
Morphism of
(G2 . (F1 . a)),
(G3 . (F1 . a)) by FUNCTOR0:33;
thus ((q1 `*` q) * F1) ! a =
(q1 `*` q) ! (F1 . a)
by A1, A2, Th12, FUNCTOR2:2
.=
(q1 ! (F1 . a)) * (q ! (F1 . a))
by A1, A2, FUNCTOR2:def 5
.=
s1F1a * (q ! (F1 . a))
by A2, Th12
.=
((q1 * F1) ! a) * ((q * F1) ! a)
by A1, A6, A5, Th12
.=
((q1 * F1) `*` (q * F1)) ! a
by A3, FUNCTOR2:def 5
;
verum end;
G1 is_transformable_to G3
by A1, A2, FUNCTOR2:2;
hence
(q1 `*` q) * F1 = (q1 * F1) `*` (q * F1)
by A4, Th10, FUNCTOR2:3; verum