let Al be QC-alphabet ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum