A3:
F is_naturally_transformable_to F2
by A1, A2, Th19;

A4: F1 is_transformable_to F2 by A2;

A5: 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) by A2, Def7;

A6: 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) by A1, Def7;

F is_transformable_to F1 by A1;

then 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) by A4, A6, A5, Lm2;

hence t2 `*` t1 is natural_transformation of F,F2 by A3, Def7; :: thesis: verum

A4: F1 is_transformable_to F2 by A2;

A5: 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) by A2, Def7;

A6: 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) by A1, Def7;

F is_transformable_to F1 by A1;

then 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) by A4, A6, A5, Lm2;

hence t2 `*` t1 is natural_transformation of F,F2 by A3, Def7; :: thesis: verum