let R be domRing; :: thesis: for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R)))
for p, q being Element of (Polynom-Ring (n,R)) st p in Ideal_ X & q in Ideal_ X holds
p + q in Ideal_ X
let n be non empty Ordinal; :: thesis: for X being Subset of (Funcs (n,([#] R)))
for p, q being Element of (Polynom-Ring (n,R)) st p in Ideal_ X & q in Ideal_ X holds
p + q in Ideal_ X
let X be Subset of (Funcs (n,([#] R))); :: thesis: for p, q being Element of (Polynom-Ring (n,R)) st p in Ideal_ X & q in Ideal_ X holds
p + q in Ideal_ X
set M = { f where f is Polynomial of n,R : X c= Zero_ f } ;
let p, q be Element of (Polynom-Ring (n,R)); :: thesis: ( p in Ideal_ X & q in Ideal_ X implies p + q in Ideal_ X )
assume A1: ( p in Ideal_ X & q in Ideal_ X ) ; :: thesis: p + q in Ideal_ X
then consider f being Polynomial of n,R such that
A2: ( f = p & X c= Zero_ f ) ;
consider g being Polynomial of n,R such that
A3: ( g = q & X c= Zero_ g ) by A1;
for y being object st y in X holds
y in Zero_ (f + g)

proof

let y be object ; :: thesis: ( y in X implies y in Zero_ (f + g) )
assume y in X ; :: thesis: y in Zero_ (f + g)
then A5: ( y in { x where x is Function of n,R : eval (f,x) = 0. R } & y in { x where x is Function of n,R : eval (g,x) = 0. R } ) by A2, A3;
then consider x1 being Function of n,R such that
A6: ( y = x1 & eval (f,x1) = 0. R ) ;
consider x2 being Function of n,R such that
A7: ( y = x2 & eval (g,x2) = 0. R ) by A5;
eval ((f + g),x1) = (0. R) + (0. R) by A7, A6, POLYNOM2:23
.= 0. R ;
hence y in Zero_ (f + g) by A6; :: thesis: verum

end;

then X c= Zero_ (f + g) ;
then f + g in Ideal_ X ;
hence p + q in Ideal_ X by A2, A3, POLYNOM1:def 11; :: thesis: verum