theorem Th34: :: SUBSTUT1:34

for A being QC-alphabet
for k being Nat
for h being FinSequence holds
( h is CQC-variable_list of k,A iff ( h is FinSequence of bound_QC-variables A & len h = k ) )