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