A3: for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds ((t1 ") . b) * (F2 /. f) = (F1 /. f) * ((t1 ") . a) by A1, A2, Lm4;
F2 is_naturally_transformable_to F1 by A1, A2, Lm5;
hence t1 " is natural_transformation of F2,F1 by A3, Def7; :: thesis: verum