set M = { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;
A1: now :: thesis: for u being object st u in { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } holds
u in the carrier of (Polynom-Ring A)
let u be object ; :: thesis: ( u in { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } implies u in the carrier of (Polynom-Ring A) )
assume u in { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ; :: thesis: u in the carrier of (Polynom-Ring A)
then ex p1 being Polynomial of A st
( u = p1 & Ext_eval (p1,x) = 0. B ) ;
hence u in the carrier of (Polynom-Ring A) by POLYNOM3:def 10; :: thesis: verum
end;
Ext_eval ((0_. A),x) = 0. B by Th17;
then 0_. A in { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } ;
hence { p where p is Polynomial of A : Ext_eval (p,x) = 0. B } is non empty Subset of (Polynom-Ring A) by A1, TARSKI:def 3; :: thesis: verum