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, Th2;

A5: F is_transformable_to F2 by A1, A2, Th2;

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, Th2;

A5: F is_transformable_to F2 by A1, A2, Th2;

now :: thesis: for a being Object of A holds ((t3 `*` t2) `*` t1) ! a = (t3 `*` (t2 `*` t1)) ! a

hence
(t3 `*` t2) `*` t1 = t3 `*` (t2 `*` t1)
by A1, A4, Th2, Th3; :: thesis: verumlet a be Object of A; :: thesis: ((t3 `*` t2) `*` t1) ! a = (t3 `*` (t2 `*` t1)) ! a

A6: <^(F2 . a),(F3 . a)^> <> {} by A3;

A7: ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, A2;

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 A7, A6, ALTCAT_1:21

.= (t3 ! a) * ((t2 `*` t1) ! a) by A1, A2, Def5

.= (t3 `*` (t2 `*` t1)) ! a by A3, A5, Def5 ; :: thesis: verum

end;A6: <^(F2 . a),(F3 . a)^> <> {} by A3;

A7: ( <^(F . a),(F1 . a)^> <> {} & <^(F1 . a),(F2 . a)^> <> {} ) by A1, A2;

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 A7, A6, ALTCAT_1:21

.= (t3 ! a) * ((t2 `*` t1) ! a) by A1, A2, Def5

.= (t3 `*` (t2 `*` t1)) ! a by A3, A5, Def5 ; :: thesis: verum