let R be domRing; :: thesis: for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds Zero_ (Ideal_ (Zero_ S)) = Zero_ S
let n be non empty Ordinal; :: thesis: for S being Subset of (Polynom-Ring (n,R)) holds Zero_ (Ideal_ (Zero_ S)) = Zero_ S
let S be Subset of (Polynom-Ring (n,R)); :: thesis: Zero_ (Ideal_ (Zero_ S)) = Zero_ S

per cases ( S <> {} or S = {} ) ;

suppose S <> {} ; :: thesis: Zero_ (Ideal_ (Zero_ S)) = Zero_ S

then reconsider S = S as non empty Subset of (Polynom-Ring (n,R)) ;
Zero_ S c= Zero_ (Ideal_ (Zero_ S)) by Th33;
hence Zero_ (Ideal_ (Zero_ S)) = Zero_ S by Th16, Th32; :: thesis: verum

end;

suppose A3: S = {} ; :: thesis: Zero_ (Ideal_ (Zero_ S)) = Zero_ S

then Zero_ (Ideal_ (Zero_ S)) = Zero_ ([#] (Polynom-Ring (n,R))) by Def6, Th30
.= {} (Funcs (n,([#] R))) by Lm4
.= Zero_ S by Def6, A3 ;
hence Zero_ (Ideal_ (Zero_ S)) = Zero_ S ; :: thesis: verum

end;

end;