:: deftheorem Def12 defines <: ISOCAT_2:def 12 :
for A, B, C being Category
for F1, G1 being Functor of A,B
for F2, G2 being Functor of A,C st F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds
for t1 being natural_transformation of F1,G1
for t2 being natural_transformation of F2,G2 holds <:t1,t2:> = <:t1,t2:>;