let R be domRing; :: thesis: for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds sqrt (Ideal_ X) = Ideal_ X
let n be non empty Ordinal; :: thesis: for X being Subset of (Funcs (n,([#] R))) holds sqrt (Ideal_ X) = Ideal_ X
let X be Subset of (Funcs (n,([#] R))); :: thesis: sqrt (Ideal_ X) = Ideal_ X

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

suppose X <> {} ; :: thesis: sqrt (Ideal_ X) = Ideal_ X

then Ideal_ X <> [#] (Polynom-Ring (n,R)) by Th30;
then reconsider IX = Ideal_ X as proper Ideal of (Polynom-Ring (n,R)) by SUBSET_1:def 6;
A4: not 1. (Polynom-Ring (n,R)) in IX by IDEAL_1:19;
sqrt (Ideal_ X) c= Ideal_ X

proof

now :: thesis: for o being object st o in sqrt (Ideal_ X) holds
o in Ideal_ X

let o be object ; :: thesis: ( o in sqrt (Ideal_ X) implies o in Ideal_ X )
assume o in sqrt (Ideal_ X) ; :: thesis: o in Ideal_ X
then consider f being Element of (Polynom-Ring (n,R)) such that
A5: ( f = o & ex m being Element of NAT st f |^ m in Ideal_ X ) ;
consider m being Element of NAT such that
A6: f |^ m in Ideal_ X by A5;
m <> 0

proof

assume A7: m = 0 ; :: thesis: contradiction
f |^ m = (power (Polynom-Ring (n,R))) . (f,m) by BINOM:def 2
.= 1_ (Polynom-Ring (n,R)) by A7, GROUP_1:def 7
.= 1. (Polynom-Ring (n,R)) ;
hence contradiction by A4, A6; :: thesis: verum

end;

then reconsider m = m as non zero Nat ;
f in [#] (Polynom-Ring (n,R)) by SUBSET_1:def 1;
then reconsider p = f as Polynomial of n,R by POLYNOM1:def 11;
consider fm being Polynomial of n,R such that
A9: ( fm = f |^ m & X c= Zero_ fm ) by A6;
f |^ m = p `^ m by BINOM:def 2;
then Zero_ fm = Zero_ {(p `^ m)} by A9, Th15
.= Zero_ {p} by Lm8
.= Zero_ p by Th15 ;
hence o in Ideal_ X by A5, A9; :: thesis: verum

end;

hence sqrt (Ideal_ X) c= Ideal_ X ; :: thesis: verum

end;

hence sqrt (Ideal_ X) = Ideal_ X by TOPZARI1:20; :: thesis: verum

end;

suppose X = {} ; :: thesis: sqrt (Ideal_ X) = Ideal_ X

then Ideal_ X = [#] (Polynom-Ring (n,R)) by Th30;
hence sqrt (Ideal_ X) = Ideal_ X by IDEAL_2:10; :: thesis: verum

end;

end;