let A, B be Category; :: thesis: for F, F1, F2 being 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 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 that

A1: F is_naturally_transformable_to F1 and

A2: 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)

A3: F1 is_transformable_to F2 by A2;

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)

reconsider t19 = t1 as transformation of F,F1 ;

reconsider t29 = t2 as transformation of F1,F2 ;

A4: F is_transformable_to F1 by A1;

thus (t2 `*` t1) . a = (t29 `*` t19) . a by A1, A2, Def8

.= (t2 . a) * (t1 . a) by A4, A3, Def5 ; :: thesis: verum

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 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 that

A1: F is_naturally_transformable_to F1 and

A2: 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)

A3: F1 is_transformable_to F2 by A2;

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)

reconsider t19 = t1 as transformation of F,F1 ;

reconsider t29 = t2 as transformation of F1,F2 ;

A4: F is_transformable_to F1 by A1;

thus (t2 `*` t1) . a = (t29 `*` t19) . a by A1, A2, Def8

.= (t2 . a) * (t1 . a) by A4, A3, Def5 ; :: thesis: verum