:: deftheorem Def14 defines NatTrans-DOMAIN NATTRA_1:def 15 :
for A, B being Category
for b₃ being non empty set holds
( b₃ is NatTrans-DOMAIN of A,B iff for x being set st x in b₃ holds
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 ) );