dom (SignGen (f,B,X)) = dom f by Def11;
then len (SignGen (f,B,X)) = len f by FINSEQ_3:29;
hence SignGen (f,B,X) is len f -element by CARD_1:def 7; :: thesis: verum