let R be domRing; :: thesis: for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X is Ideal of (Polynom-Ring (n,R))
let n be non empty Ordinal; :: thesis: for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X is Ideal of (Polynom-Ring (n,R))
let X be Subset of (Funcs (n,([#] R))); :: thesis: Ideal_ X is Ideal of (Polynom-Ring (n,R))
A1: Ideal_ X is add-closed by Lm5;
Ideal_ X is right-ideal by Lm7;
hence Ideal_ X is Ideal of (Polynom-Ring (n,R)) by A1; :: thesis: verum