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