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