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