let R be domRing; :: thesis: for n being non empty Ordinal
for S, T being non empty Subset of (Polynom-Ring (n,R)) st S c= T holds
Zero_ T c= Zero_ S
let n be non empty Ordinal; :: thesis: for S, T being non empty Subset of (Polynom-Ring (n,R)) st S c= T holds
Zero_ T c= Zero_ S
let S, T be non empty Subset of (Polynom-Ring (n,R)); :: thesis: ( S c= T implies Zero_ T c= Zero_ S )
assume A1: S c= T ; :: thesis: Zero_ T c= Zero_ S
for o being object st o in Zero_ T holds
o in Zero_ S

proof

let o be object ; :: thesis: ( o in Zero_ T implies o in Zero_ S )
assume o in Zero_ T ; :: thesis: o in Zero_ S
then o in { x where x is Function of n,R : for f being Polynomial of n,R st f in T 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 T holds
eval (f,x) = 0. R ) ) ;
for f being Polynomial of n,R st f in S holds
eval (f,x) = 0. R by A1, A3;
then x 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 } ;
hence o in Zero_ S by A3, Def6; :: thesis: verum

end;

hence Zero_ T c= Zero_ S ; :: thesis: verum