let A, B be Category; :: thesis: 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; :: 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 that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 and
A3: 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)
A4: F1 is_transformable_to F3 by A2, A3, Th19;
A5: F is_transformable_to F2 by A1, A2, Th19;

now

let a be Object of A; :: thesis: ((t3 `*` t2) `*` t1) . a = (t3 `*` (t2 `*` t1)) . a
A6: Hom (F . a),(F1 . a) <> {} by A1, Def2;
A7: Hom (F1 . a),(F2 . a) <> {} by A2, Def2;
A8: Hom (F2 . a),(F3 . a) <> {} by A3, Def2;
thus ((t3 `*` t2) `*` t1) . a = ((t3 `*` t2) . a) * (t1 . a) by A1, A4, Def6
.= ((t3 . a) * (t2 . a)) * (t1 . a) by A2, A3, Def6
.= (t3 . a) * ((t2 . a) * (t1 . a)) by A6, A7, A8, CAT_1:54
.= (t3 . a) * ((t2 `*` t1) . a) by A1, A2, Def6
.= (t3 `*` (t2 `*` t1)) . a by A3, A5, Def6 ; :: thesis: verum

end;

hence (t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1) by A1, A4, Th19, Th20; :: thesis: verum