set f = the Function of NAT,NAT;
take the Function of NAT,NAT ; :: thesis: dom the Function of NAT,NAT = NAT
thus dom the Function of NAT,NAT = NAT by FUNCT_2:def 1; :: thesis: verum