let A be array; :: thesis: ( A = {[a,x]} implies A is natural-valued )
assume A = {[a,x]} ; :: thesis: A is natural-valued
then rng A = {x} by FUNCT_5:12;
then rng A c= NAT by MEMBERED:6;
hence A is natural-valued ; :: thesis: verum