dom (f + x) = dom f by VALUED_1:def 2;
then len (f + x) = len f by FINSEQ_3:29;
then (f + x) null f is len f -element ;
hence f + x is len f -element ; :: thesis: verum