let A, B be Category; for F, F1, F2, F3 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 holds
for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let F, F1, F2, F3 be Functor of A,B; ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 implies for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) )
assume that
A1:
F is_transformable_to F1
and
A2:
F1 is_transformable_to F2
and
A3:
F2 is_transformable_to F3
; for t1 being transformation of F,F1
for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t1 be transformation of F,F1; for t2 being transformation of F1,F2
for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t2 be transformation of F1,F2; for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t3 be transformation of F2,F3; (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
A4:
F1 is_transformable_to F3
by A2, A3, Th14;
A5:
F is_transformable_to F2
by A1, A2, Th14;
now for a being Object of A holds ((t3 `*` t2) `*` t1) . a = (t3 `*` (t2 `*` t1)) . alet a be
Object of
A;
((t3 `*` t2) `*` t1) . a = (t3 `*` (t2 `*` t1)) . aA6:
Hom (
(F . a),
(F1 . a))
<> {}
by A1;
A7:
Hom (
(F1 . a),
(F2 . a))
<> {}
by A2;
A8:
Hom (
(F2 . a),
(F3 . a))
<> {}
by A3;
thus ((t3 `*` t2) `*` t1) . a =
((t3 `*` t2) . a) * (t1 . a)
by A1, A4, Def5
.=
((t3 . a) * (t2 . a)) * (t1 . a)
by A2, A3, Def5
.=
(t3 . a) * ((t2 . a) * (t1 . a))
by A6, A7, A8, CAT_1:25
.=
(t3 . a) * ((t2 `*` t1) . a)
by A1, A2, Def5
.=
(t3 `*` (t2 `*` t1)) . a
by A3, A5, Def5
;
verum end;
hence
(t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
by A1, A4, Th14, Th15; verum