let Al be QC-alphabet ; for Al2 being Al -expanding QC-alphabet
for k being Nat
for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2
let Al2 be Al -expanding QC-alphabet ; for k being Nat
for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2
let k be Nat; for l being CQC-variable_list of k,Al holds l is CQC-variable_list of k,Al2
let l be CQC-variable_list of k,Al; l is CQC-variable_list of k,Al2
( rng l c= bound_QC-variables Al & bound_QC-variables Al c= bound_QC-variables Al2 )
by Th4;
then
rng l c= bound_QC-variables Al2
;
hence
l is CQC-variable_list of k,Al2
by FINSEQ_1:def 4, XBOOLE_1:1; verum