( len (Subst (l,f)) = len l & len l = k ) by Def1, CARD_1:def 7;
hence Subst (l,f) is k -element by CARD_1:def 7; :: thesis: verum