reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
dom f = NAT by ds;
then f . i1 in rng f by FUNCT_1:3;
hence f . i is Field ; :: thesis: verum