reconsider l9 = l as FinSequence of bound_QC-variables by Lm2;
reconsider h = f * l9 as FinSequence of bound_QC-variables by FINSEQ_2:36;
len h = len l9 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