consider IT being empty Function;
take IT ; :: thesis: ( IT is finite & IT is NAT -defined )
thus IT is finite ; :: thesis: IT is NAT -defined
thus dom IT c= NAT ; :: according to RELAT_1:def 18 :: thesis: verum