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

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