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 FINSEQ_1:def 18 ;
hence l * f is CQC-variable_list of by Lm2; :: thesis: verum