reconsider n = n as Element of NAT by ORDINAL1:def 13;
f . n is Element of D ;
hence f . n is Element of D ; :: thesis: verum