theorem Th59: :: SUBLEMMA:59

for Al being QC-alphabet
for k being Nat
for A being non empty set
for v being Element of Valuations_in (Al,A)
for ll being CQC-variable_list of k,Al holds v *' ll = ll * (v | (still_not-bound_in ll))