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