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