0 + 1 <= len f by A1, NAT_1:13;
then len f in dom f by FINSEQ_3:25;
then f . (len f) in rng f by FUNCT_1:3;
hence f . (len f) is Element of D ; :: thesis: verum