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