reconsider l' = l as FinSequence of bound_QC-variables by Lm2;
reconsider h = f * l' as FinSequence of bound_QC-variables by FINSEQ_2:36;
len h = len l' by FINSEQ_2:37
.= k by FINSEQ_1:def 18 ;
hence l * f is CQC-variable_list of k by FINSEQ_1:def 18, FINSEQ_2:27; :: thesis: verum