let A, B be Category; 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; ( 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
; 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; ( ( 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)
; 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; ( ( 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)
; 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; ( 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) <> {}
; 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; ((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
; verum