dom (a (#) f) = dom f by VALUED_1:def 5;
then len (a (#) f) = len f by FINSEQ_3:29;
then (a (#) f) null f is len f -element ;
hence a (#) f is len f -element ; :: thesis: verum