n is Element of NAT by ORDINAL1:def 13;
then f . n in rng f by FUNCT_2:189;
hence f . n is Subset of E ; :: thesis: verum