let R be domRing; :: thesis: for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R)))
for a, p being Element of (Polynom-Ring (n,R)) st p in Ideal_ X holds
a * p in Ideal_ X
let n be non empty Ordinal; :: thesis: for X being Subset of (Funcs (n,([#] R)))
for a, p being Element of (Polynom-Ring (n,R)) st p in Ideal_ X holds
a * p in Ideal_ X
let X be Subset of (Funcs (n,([#] R))); :: thesis: for a, p being Element of (Polynom-Ring (n,R)) st p in Ideal_ X holds
a * p in Ideal_ X
let a, p be Element of (Polynom-Ring (n,R)); :: thesis: ( p in Ideal_ X implies a * p in Ideal_ X )
assume A1: p in Ideal_ X ; :: thesis: a * p in Ideal_ X
p in [#] (Polynom-Ring (n,R)) by SUBSET_1:def 1;
then reconsider a1 = a as Polynomial of n,R by POLYNOM1:def 11;
consider f being Polynomial of n,R such that
A2: ( f = p & X c= Zero_ f ) by A1;
for y being object st y in X holds
y in Zero_ (a1 *' f)

proof

let y be object ; :: thesis: ( y in X implies y in Zero_ (a1 *' f) )
assume y in X ; :: thesis: y in Zero_ (a1 *' f)
then y in { x where x is Function of n,R : eval (f,x) = 0. R } by A2;
then consider x1 being Function of n,R such that
A4: ( y = x1 & eval (f,x1) = 0. R ) ;
eval ((a1 *' f),x1) = (eval (a1,x1)) * (0. R) by A4, POLYNOM2:25
.= 0. R ;
hence y in Zero_ (a1 *' f) by A4; :: thesis: verum

end;

then X c= Zero_ (a1 *' f) ;
then a1 *' f in Ideal_ X ;
hence a * p in Ideal_ X by A2, POLYNOM1:def 11; :: thesis: verum