let R be domRing; :: thesis: for n being non empty Ordinal
for S being non empty Subset of (Polynom-Ring (n,R)) holds Zero_ S = Zero_ (S -Ideal)
let n be non empty Ordinal; :: thesis: for S being non empty Subset of (Polynom-Ring (n,R)) holds Zero_ S = Zero_ (S -Ideal)
let S be non empty Subset of (Polynom-Ring (n,R)); :: thesis: Zero_ S = Zero_ (S -Ideal)
A1: S c= S -Ideal by IDEAL_1:def 14;
Zero_ S c= Zero_ (S -Ideal)

proof

set MS = { x where x is Function of n,R : for f being Polynomial of n,R st f in S holds
eval (f,x) = 0. R } ;
set MI = { x where x is Function of n,R : for f being Polynomial of n,R st f in S -Ideal holds
eval (f,x) = 0. R } ;
for o being object st o in Zero_ S holds
o in Zero_ (S -Ideal)

proof

let o be object ; :: thesis: ( o in Zero_ S implies o in Zero_ (S -Ideal) )
assume o in Zero_ S ; :: thesis: o in Zero_ (S -Ideal)
then o in { x where x is Function of n,R : for f being Polynomial of n,R st f in S holds
eval (f,x) = 0. R } by Def6;
then consider x being Function of n,R such that
A3: ( o = x & ( for f being Polynomial of n,R st f in S holds
eval (f,x) = 0. R ) ) ;
for p being Polynomial of n,R st p in S -Ideal holds
eval (p,x) = 0. R

proof

let p be Polynomial of n,R; :: thesis: ( p in S -Ideal implies eval (p,x) = 0. R )
assume p in S -Ideal ; :: thesis: eval (p,x) = 0. R
then consider F being LinearCombination of S such that
A5: p = Sum F by IDEAL_1:60;
A6: for i being Nat st i in dom (E_eval (F,x)) holds
(E_eval (F,x)) . i = 0. R

proof

let i be Nat; :: thesis: ( i in dom (E_eval (F,x)) implies (E_eval (F,x)) . i = 0. R )
assume i in dom (E_eval (F,x)) ; :: thesis: (E_eval (F,x)) . i = 0. R
then A8: i in dom F by Def2;
consider u, v being Element of (Polynom-Ring (n,R)), a being Element of S such that
A9: F /. i = (u * a) * v by A8, IDEAL_1:def 8;
A10: a in S by SUBSET_1:def 1;
a in Polynom-Ring (n,R) by SUBSET_1:def 1;
then reconsider a1 = a as Polynomial of n,R by POLYNOM1:def 11;
A11: E_eval (a,x) = eval (a1,x) by Def1
.= 0. R by A10, A3 ;
F /. i = (u * v) * a by A9, GROUP_1:def 3;
then (E_eval (F,x)) . i = E_eval (((u * v) * a),x) by A8, Def2
.= (E_eval ((u * v),x)) * (0. R) by A11, Th3
.= 0. R ;
hence (E_eval (F,x)) . i = 0. R ; :: thesis: verum

end;

A13: Sum (E_eval (F,x)) = Sum ((len (E_eval (F,x))) |-> (0. R)) by A6, Lm1
.= 0. R by Lm2 ;
eval (p,x) = E_eval ((Sum F),x) by A5, Def1
.= 0. R by A13, Th5 ;
hence eval (p,x) = 0. R ; :: thesis: verum

end;

then x in { x where x is Function of n,R : for f being Polynomial of n,R st f in S -Ideal holds
eval (f,x) = 0. R } ;
hence o in Zero_ (S -Ideal) by A3, Def6; :: thesis: verum

end;

hence Zero_ S c= Zero_ (S -Ideal) ; :: thesis: verum

end;

hence Zero_ S = Zero_ (S -Ideal) by A1, Th16; :: thesis: verum