let A, B be Category; :: thesis: for F, F1, F2 being Functor of A,B st F is_transformable_to F1 & F1 is_transformable_to F2 holds

for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let F, F1, F2 be Functor of A,B; :: thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume that

A1: F is_transformable_to F1 and

A2: F1 is_transformable_to F2 ; :: thesis: for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let t1 be transformation of F,F1; :: thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) implies for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume A3: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; :: thesis: for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let t2 be transformation of F1,F2; :: thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) implies for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume A4: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

A5: Hom ((F . b),(F1 . b)) <> {} by A1;

A6: Hom ((F . a),(F1 . a)) <> {} by A1;

A7: Hom ((F1 . b),(F2 . b)) <> {} by A2;

A8: Hom ((F1 . a),(F2 . a)) <> {} by A2;

assume A9: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

then A10: Hom ((F . a),(F . b)) <> {} by CAT_1:84;

let f be Morphism of a,b; :: thesis: ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

A11: Hom ((F2 . a),(F2 . b)) <> {} by A9, CAT_1:84;

A12: Hom ((F1 . a),(F1 . b)) <> {} by A9, CAT_1:84;

thus ((t2 `*` t1) . b) * (F /. f) = ((t2 . b) * (t1 . b)) * (F /. f) by A1, A2, Def5

.= (t2 . b) * ((t1 . b) * (F /. f)) by A10, A5, A7, CAT_1:25

.= (t2 . b) * ((F1 /. f) * (t1 . a)) by A3, A9

.= ((t2 . b) * (F1 /. f)) * (t1 . a) by A6, A7, A12, CAT_1:25

.= ((F2 /. f) * (t2 . a)) * (t1 . a) by A4, A9

.= (F2 /. f) * ((t2 . a) * (t1 . a)) by A6, A8, A11, CAT_1:25

.= (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, Def5 ; :: thesis: verum

for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let F, F1, F2 be Functor of A,B; :: thesis: ( F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume that

A1: F is_transformable_to F1 and

A2: F1 is_transformable_to F2 ; :: thesis: for t1 being transformation of F,F1 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) holds

for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let t1 be transformation of F,F1; :: thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ) implies for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume A3: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t1 . b) * (F /. f) = (F1 /. f) * (t1 . a) ; :: thesis: for t2 being transformation of F1,F2 st ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) holds

for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let t2 be transformation of F1,F2; :: thesis: ( ( for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ) implies for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

assume A4: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds (t2 . b) * (F1 /. f) = (F2 /. f) * (t2 . a) ; :: thesis: for a, b being Object of A st Hom (a,b) <> {} holds

for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

let a, b be Object of A; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a) )

A5: Hom ((F . b),(F1 . b)) <> {} by A1;

A6: Hom ((F . a),(F1 . a)) <> {} by A1;

A7: Hom ((F1 . b),(F2 . b)) <> {} by A2;

A8: Hom ((F1 . a),(F2 . a)) <> {} by A2;

assume A9: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

then A10: Hom ((F . a),(F . b)) <> {} by CAT_1:84;

let f be Morphism of a,b; :: thesis: ((t2 `*` t1) . b) * (F /. f) = (F2 /. f) * ((t2 `*` t1) . a)

A11: Hom ((F2 . a),(F2 . b)) <> {} by A9, CAT_1:84;

A12: Hom ((F1 . a),(F1 . b)) <> {} by A9, CAT_1:84;

thus ((t2 `*` t1) . b) * (F /. f) = ((t2 . b) * (t1 . b)) * (F /. f) by A1, A2, Def5

.= (t2 . b) * ((t1 . b) * (F /. f)) by A10, A5, A7, CAT_1:25

.= (t2 . b) * ((F1 /. f) * (t1 . a)) by A3, A9

.= ((t2 . b) * (F1 /. f)) * (t1 . a) by A6, A7, A12, CAT_1:25

.= ((F2 /. f) * (t2 . a)) * (t1 . a) by A4, A9

.= (F2 /. f) * ((t2 . a) * (t1 . a)) by A6, A8, A11, CAT_1:25

.= (F2 /. f) * ((t2 `*` t1) . a) by A1, A2, Def5 ; :: thesis: verum