p in nonConstantPolys F ;
then p in dom g by FUNCT_2:def 1;
then A: g . p in rng g by FUNCT_1:3;
rng g c= card (nonConstantPolys F) by RELAT_1:def 19;
hence g . p is Ordinal by A; :: thesis: verum