reconsider l9 = l as FinSequence of bound_QC-variables A by Lm2;
reconsider h = f * l9 as FinSequence of bound_QC-variables A by FINSEQ_2:32;
len h = len l9 by FINSEQ_2:33
.= k by CARD_1:def 7 ;
hence l * f is CQC-variable_list of k,A by CARD_1:def 7, FINSEQ_2:24; :: thesis: verum