( <:F1,F2:> is_naturally_transformable_to <:G1,G2:> & ( for a, b being Object of A st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (<:t1,t2:> . b) * (<:F1,F2:> /. f) = (<:G1,G2:> /. f) * (<:t1,t2:> . a) ) ) by A1, Lm4, Th36;
hence <:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:> by NATTRA_1:def 8; :: thesis: verum