:: deftheorem defines denamingSeq NOMIN_8:def 8 :
for V, A being set
for val being FinSequence
for b₄ being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) holds
( b₄ = denamingSeq (V,A,val) iff ( len b₄ = len val & ( for n being Nat st 1 <= n & n <= len b₄ holds
b₄ . n = denaming (V,A,(val . n)) ) ) );