set A = DTConUA f,D;
A2: [s,p] in the Rules of (DTConUA f,D) by A1, LANG1:def 1;
reconsider s0 = s as Element of (dom f) \/ D ;
reconsider p0 = p as Element of ((dom f) \/ D) * by A2, ZFMISC_1:106;
[s0,p0] in REL f,D by A1, LANG1:def 1;
then s0 in dom f by Def8;
hence s is Element of NAT ; :: thesis: verum