( len (Subst l,f) = len l & len l = k ) by Def3, FINSEQ_1:def 18;
hence Subst l,f is QC-variable_list of k by FINSEQ_1:def 18; :: thesis: verum