let x be Element of NatMinor f; :: thesis: x is natural-valued
rng x c= NAT by FUNCT_2:92;
hence x is natural-valued by VALUED_0:def 6; :: thesis: verum