set M = { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } ;

now :: thesis: for u being object st u in { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } holds
u in [#] (Polynom-Ring (n,R))

let u be object ; :: thesis: ( u in { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } implies u in [#] (Polynom-Ring (n,R)) )
assume u in { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } ; :: thesis: u in [#] (Polynom-Ring (n,R))
then consider f being Polynomial of n,R such that
A2: ( u = f & ex i being Element of n st f = deg1Poly (a,i) ) ;
thus u in [#] (Polynom-Ring (n,R)) by A2, POLYNOM1:def 11; :: thesis: verum

end;

then reconsider M = { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } as Subset of (Polynom-Ring (n,R)) by TARSKI:def 3;
not M is empty

proof

reconsider k = 0 as Element of n by ORDINAL3:8;
deg1Poly (a,k) in M ;
hence not M is empty ; :: thesis: verum

end;

hence { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } is non empty Subset of (Polynom-Ring (n,R)) ; :: thesis: verum