:: deftheorem Def7 defines SCassignment NOMIN_2:def 7 :
for V, A being set
for v being object
for b₄ being Function of (FPrg (ND (V,A))),(FPrg (ND (V,A))) holds
( b₄ = SCassignment (V,A,v) iff for f being SCBinominativeFunction of V,A holds
( dom (b₄ . f) = dom f & ( for d being TypeSCNominativeData of V,A st d in dom (b₄ . f) holds
(b₄ . f) . d = local_overlapping (V,A,d,(f . d),v) ) ) );