let F be NAT -defined non empty initial Function; :: thesis: 0 in dom F
consider x being set such that
A1: x in dom F by XBOOLE_0:def 1;
dom F c= NAT by RELAT_1:def 18;
then reconsider x = x as Element of NAT by A1;
( x = 0 or 0 < x ) ;
hence 0 in dom F by A1, Def13; :: thesis: verum