let R be domRing; :: thesis: for n being non empty Ordinal
for p being Polynomial of n,R holds Zero_ {p} = Zero_ p
let n be non empty Ordinal; :: thesis: for p being Polynomial of n,R holds Zero_ {p} = Zero_ p
let p be Polynomial of n,R; :: thesis: Zero_ {p} = Zero_ p
set S = {p};
thus for o being object st o in Zero_ {p} holds
o in Zero_ p :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Zero_ p c= Zero_ {p}

proof

let o be object ; :: thesis: ( o in Zero_ {p} implies o in Zero_ p )
assume o in Zero_ {p} ; :: thesis: o in Zero_ p
then o in { x where x is Function of n,R : for f being Polynomial of n,R st f in {p} holds
eval (f,x) = 0. R } by Def6;
then consider x being Function of n,R such that
A3: ( x = o & ( for f being Polynomial of n,R st f in {p} holds
eval (f,x) = 0. R ) ) ;
assume not o in Zero_ p ; :: thesis: contradiction
then A5: eval (p,x) <> 0. R by A3;
p in {p} by TARSKI:def 1;
hence contradiction by A5, A3; :: thesis: verum

end;

thus for o being object st o in Zero_ p holds
o in Zero_ {p} :: according to TARSKI:def 3 :: thesis: verum

proof

let o be object ; :: thesis: ( o in Zero_ p implies o in Zero_ {p} )
assume o in Zero_ p ; :: thesis: o in Zero_ {p}
then consider x1 being Function of n,R such that
A6: ( x1 = o & eval (p,x1) = 0. R ) ;
for f being Polynomial of n,R st f in {p} holds
eval (f,x1) = 0. R by A6, TARSKI:def 1;
then x1 in { x where x is Function of n,R : for f being Polynomial of n,R st f in {p} holds
eval (f,x) = 0. R } ;
hence o in Zero_ {p} by A6, Def6; :: thesis: verum

end;