:: deftheorem Def19 defines NForms MSAFREE4:def 19 :
for I being non empty set
for X being V5() ManySortedSet of I
for R being terminating with_UN_property ManySortedRelation of X
for b₄ being V5() ManySortedSubset of X holds
( b₄ = NForms R iff for i being Element of I holds b₄ . i = { (nf (x,(R . i))) where x is Element of X . i : verum } );