let A, B be category; :: thesis: for F, F1, F2, F3 being covariant Functor of A,B

for t being natural_transformation of F,F1

for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let F, F1, F2, F3 be covariant Functor of A,B; :: thesis: for t being natural_transformation of F,F1

for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let t be natural_transformation of F,F1; :: thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let t1 be natural_transformation of F1,F2; :: thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) )

assume that

A1: F is_naturally_transformable_to F1 and

A2: F1 is_naturally_transformable_to F2 and

A3: F2 is_naturally_transformable_to F3 ; :: thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

A4: F is_naturally_transformable_to F2 by A1, A2, Th8;

let t3 be natural_transformation of F2,F3; :: thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

A5: F2 is_transformable_to F3 by A3;

A6: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, A2;

F1 is_naturally_transformable_to F3 by A2, A3, Th8;

hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def8

.= (t3 `*` t1) `*` t by A2, A3, Def8

.= t3 `*` (t1 `*` t) by A6, A5, Th6

.= t3 `*` (t1 `*` t) by A1, A2, Def8

.= t3 `*` (t1 `*` t) by A3, A4, Def8 ;

:: thesis: verum

for t being natural_transformation of F,F1

for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let F, F1, F2, F3 be covariant Functor of A,B; :: thesis: for t being natural_transformation of F,F1

for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let t be natural_transformation of F,F1; :: thesis: for t1 being natural_transformation of F1,F2 st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 holds

for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

let t1 be natural_transformation of F1,F2; :: thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t) )

assume that

A1: F is_naturally_transformable_to F1 and

A2: F1 is_naturally_transformable_to F2 and

A3: F2 is_naturally_transformable_to F3 ; :: thesis: for t3 being natural_transformation of F2,F3 holds (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

A4: F is_naturally_transformable_to F2 by A1, A2, Th8;

let t3 be natural_transformation of F2,F3; :: thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)

A5: F2 is_transformable_to F3 by A3;

A6: ( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, A2;

F1 is_naturally_transformable_to F3 by A2, A3, Th8;

hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def8

.= (t3 `*` t1) `*` t by A2, A3, Def8

.= t3 `*` (t1 `*` t) by A6, A5, Th6

.= t3 `*` (t1 `*` t) by A1, A2, Def8

.= t3 `*` (t1 `*` t) by A3, A4, Def8 ;

:: thesis: verum