let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F, F1, F2 being covariant Functor of A,B st F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 holds
for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let F, F1, F2 be covariant Functor of A,B; :: thesis: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 implies for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) )
assume A1: ( F is_naturally_transformable_to F1 & F1 is_naturally_transformable_to F2 ) ; :: thesis: for t1 being natural_transformation of F,F1
for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let t1 be natural_transformation of F,F1; :: thesis: for t2 being natural_transformation of F1,F2
for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let t2 be natural_transformation of F1,F2; :: thesis: for a being object of A holds (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
let a be object of A; :: thesis: (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a)
( F is_transformable_to F1 & F1 is_transformable_to F2 ) by A1, Def6;
hence (t2 `*` t1) ! a = (t2 ! a) * (t1 ! a) by Def5; :: thesis: verum