:: deftheorem Def8 defines initial_assignments_Seq NOMIN_7:def 8 :
for V, A being set
for loc being b₁ -valued Function
for val being Function
for size being Nat st 0 < size holds
for b₆ being FinSequence of PFuncs ((ND (V,A)),(ND (V,A))) holds
( b₆ = initial_assignments_Seq (A,loc,val,size) iff ( len b₆ = size & b₆ . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) & ( for n being Nat st 1 <= n & n < size holds
b₆ . (n + 1) = PP_composition ((b₆ . n),(SC_assignment ((denaming (V,A,(val . (n + 1)))),(loc /. (n + 1))))) ) ) );