let A, B be Category; :: thesis: for F, F1, F2, F3 being 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 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, Th25;
A5: F2 is_transformable_to F3 by A3, Def7;
A6: F1 is_transformable_to F2 by A2, Def7;
let t3 be natural_transformation of F2,F3; :: thesis: (t3 `*` t1) `*` t = t3 `*` (t1 `*` t)
A7: F is_transformable_to F1 by A1, Def7;
F1 is_naturally_transformable_to F3 by A2, A3, Th25;
hence (t3 `*` t1) `*` t = (t3 `*` t1) `*` t by A1, Def9
.= (t3 `*` t1) `*` t by A2, A3, Def9
.= t3 `*` (t1 `*` t) by A7, A6, A5, Th23
.= t3 `*` (t1 `*` t) by A1, A2, Def9
.= t3 `*` (t1 `*` t) by A3, A4, Def9 ;
:: thesis: verum