let A, B be category; :: thesis: for F, F1, F2, F3 being covariant 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 covariant Functor of A,B; :: thesis: ( 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 A1:
( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 )
; :: thesis: 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; :: thesis: 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; :: thesis: for t3 being transformation of F2,F3 holds (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
let t3 be transformation of F2,F3; :: thesis: (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
A2:
( F is_transformable_to F2 & F1 is_transformable_to F3 )
by A1, Th4;
then A3:
F is_transformable_to F3
by A1, Th4;
now let a be
object of
A;
:: thesis: ((t3 `*` t2) `*` t1) ! a = (t3 `*` (t2 `*` t1)) ! aA4:
(
<^(F . a),(F1 . a)^> <> {} &
<^(F1 . a),(F2 . a)^> <> {} &
<^(F2 . a),(F3 . a)^> <> {} )
by A1, Def1;
thus ((t3 `*` t2) `*` t1) ! a =
((t3 `*` t2) ! a) * (t1 ! a)
by A1, A2, Def5
.=
((t3 ! a) * (t2 ! a)) * (t1 ! a)
by A1, Def5
.=
(t3 ! a) * ((t2 ! a) * (t1 ! a))
by A4, ALTCAT_1:25
.=
(t3 ! a) * ((t2 `*` t1) ! a)
by A1, Def5
.=
(t3 `*` (t2 `*` t1)) ! a
by A1, A2, Def5
;
:: thesis: verum end;
hence
(t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
by A3, Th5; :: thesis: verum