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