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