:: deftheorem Def15 defines NatTrans NATTRA_1:def 16 :
for A, B being Category
for b₃ being NatTrans-DOMAIN of A,B holds
( b₃ = NatTrans (A,B) iff for x being set holds
( x in b₃ iff ex F1, F2 being Functor of A,B ex t being natural_transformation of F1,F2 st
( x = [[F1,F2],t] & F1 is_naturally_transformable_to F2 ) ) );