theorem Th10: :: SUBLEMMA:10

for Al being QC-alphabet
for k being Nat
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds CQC_Subst (ll,Sub) is CQC-variable_list of k,Al