A: now :: thesis: for o being object st o in { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } holds
o in the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F))

let o be object ; :: thesis: ( o in { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } implies o in the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) )
assume o in { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ; :: thesis: o in the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F))
then consider p being non constant Element of the carrier of (Polynom-Ring F) such that
A: o = Poly ((g . p),p) ;
thus o in the carrier of (Polynom-Ring ((card (nonConstantPolys F)),F)) by A, POLYNOM1:def 11; :: thesis: verum

end;

set p = the non constant Element of the carrier of (Polynom-Ring F);
Poly ((g . the non constant Element of the carrier of (Polynom-Ring F)), the non constant Element of the carrier of (Polynom-Ring F)) in { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;
hence { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } is non empty Subset of (Polynom-Ring ((card (nonConstantPolys F)),F)) by A, TARSKI:def 3; :: thesis: verum