theorem Th13: :: CQC_SIM1:13

for A being QC-alphabet
for k being Nat
for l being CQC-variable_list of k,A
for i being Nat st 1 <= i & i <= len l holds
l . i in bound_QC-variables A