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: F1 is_naturally_transformable_to F3 by A2, A3, Th10;
A5: F is_naturally_transformable_to F2 by A1, A2, Th10;
A6: ( F is_transformable_to F1 & F1 is_transformable_to F2 & F2 is_transformable_to F3 ) by A1, A2, A3, Def6;
let t3 be natural_transformation of F2,F3; :: thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
thus (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, A4, Def8
.= (t3 `*` t1) `*` t by A2, A3, Def8
.= t3 `*` (t1 `*` t) by A6, Th8
.= t3 `*` (t1 `*` t) by A1, A2, Def8
.= t3 `*` (t1 `*` t) by A3, A5, Def8 ; :: thesis: verum