dom f = NAT by ds;
then f . i in rng f by FUNCT_1:3;
hence f . i is Field by defFy; :: thesis: verum