:: deftheorem Def3 defines *' VALUAT_1:def 3 :
for Al being QC-alphabet
for A being non empty set
for k being Nat
for ll being CQC-variable_list of k,Al
for v being Element of Valuations_in (Al,A)
for b₆ being FinSequence of A holds
( b₆ = v *' ll iff ( len b₆ = k & ( for i being Nat st 1 <= i & i <= k holds
b₆ . i = v . (ll . i) ) ) );