:: deftheorem Def4 defines NDdataSeq NOMIN_2:def 4 :
for g being Function-yielding Function
for X being Function
for d being object
for b₄ being Function holds
( b₄ = NDdataSeq (g,X,d) iff ( dom b₄ = dom X & ( for x being object st x in dom X holds
b₄ . x = [(X . x),((g . x) . d)] ) ) );